1  /-
  2  Copyright (c) 2018 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl
  5  -/
  6  import data.set.finite group_theory.coset data.nat.totient
src         └─────────────┘ └────────────────┘ └──────────────┘
  7  open function
  8  
  9  variables {α : Type*} {s : set α} {a a₁ a₂ b c: α}
id                              └─┘
src                             └─┘
typ                             └─┘
 10  
 11  -- TODO this lemma isn't used anywhere in this file, and should be moved elsewhere.
 12  namespace finset
 13  open finset
 14  
 15  lemma mem_range_iff_mem_finset_range_of_mod_eq [decidable_eq α] {f : ℤ → α} {a : α} {n : ℕ}
id                                                   └──────────┘                         
src                                                  └──────────┘                           
typ                                                  └──────────┘                         
 16    (hn : 0 < n) (h : ∀i, f (i % n) = f i) :
id                                
src                                  
typ                               
 17    a ∈ set.range f ↔ a ∈ (finset.range n).image (λi, f i) :=
id       └───────┘      └──────────┘  └───┘       
src       └───────┘        └──────────┘   └───┘
typ      └───────┘      └──────────┘  └───┘       
doc        └───────┘          └──────────┘   └───┘
 18  suffices (∃i, f (i % n) = a) ↔ ∃i, i < n ∧ f ↑i = a, by simpa [h],
id                                            
src                                               └─────┘ 
typ                                    └─────┘
doc                                                          └─────┘ 
txt                                                          └─────┘ 
par                                                          └─────┘ 
pid                                                                
st                                                          └────────┘
 19  have hn' : 0 < (n : ℤ), from int.coe_nat_lt.mpr hn,
id                             └────────────┘└──┘ └┘
src                             └────────────┘└──┘
typ                            └────────────┘└──┘ └┘
 20  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
 21    (assume ⟨i, hi⟩,
id             
typ            
 22      have 0 ≤ i % ↑n, from int.mod_nonneg _ (ne_of_gt hn'),
id                         └────────────┘    └──────┘ └─┘
src                         └────────────┘    └──────┘
typ                        └────────────┘    └──────┘ └─┘
 23      ⟨int.to_nat (i % n),
id        └────────┘     
src       └────────┘    
typ       └────────┘     
 24        by rw [←int.coe_nat_lt, int.to_nat_of_nonneg this]; exact ⟨int.mod_lt_of_pos i hn', hi⟩⟩)
id                 └────────────┘  └──────────────────┘ └──┘          └───────────────┘  └─┘  └┘
src           └───┘└────────────┘└┘└──────────────────┘      └────┘ └───────────────┘    └┘  
typ           └───┘└────────────┘└┘└──────────────────┘└──┘  └────┘ └───────────────┘└─┘└┘└┘
doc           └───┘              └┘                          └────┘                      └┘  
txt           └───┘              └┘                          └────┘                      └┘  
par           └───┘              └┘                          └────┘                      └┘  
pid             └─┘              └┘                                                     └┘  
st           └──────────────────┘└─────────────────────────┘└───────────────────────────────────┘
 25    (assume ⟨i, hi, ha⟩,
id             
typ            
 26      ⟨i, by rw [int.mod_eq_of_lt (int.coe_zero_le _) (int.coe_nat_lt_coe_nat_of_lt hi), ha]⟩)
id                  └──────────────┘  └─────────────┘     └──────────────────────────┘ └┘   └┘
src             └──┘└──────────────┘ └─────────────┘└──┘ └──────────────────────────┘  └─┘  
typ             └──┘└──────────────┘ └─────────────┘└──┘ └──────────────────────────┘└┘└─┘└┘
doc             └──┘                                └──┘                               └─┘  
txt             └──┘                                └──┘                               └─┘  
par             └──┘                                └──┘                               └─┘  
pid               └┘                                └──┘                               └─┘  
st             └─────────────────────────────────────────────────────────────────────────┘└──┘
 27  
 28  end finset
 29  
 30  lemma conj_inj [group α] {x : α} : function.injective (λ (g : α), x * g * x⁻¹) :=
id                   └───┘            └────────────────┘                └┘
src                  └───┘              └────────────────┘                    └┘
typ                  └───┘            └────────────────┘                └┘
 31  λ a b h, by simpa [mul_left_inj, mul_right_inj] using h
id                   └──────────┘  └───────────┘        
src              └─────┘└──────────┘└┘└───────────┘└──────┘ 
typ           └─────┘└──────────┘└┘└───────────┘└──────┘
doc              └─────┘            └┘             └──────┘ 
txt              └─────┘            └┘             └──────┘ 
par              └─────┘            └┘             └──────┘ 
pid                               └┘             └────┘ 
st              └────────────────────────────────────────────
 32  
src  
typ  
doc  
txt  
par  
pid  
st   
 33  lemma mem_normalizer_fintype [group α] {s : set α} [fintype s] {x : α}
id                                 └───┘        └─┘    └─────┘        
src                                └───┘         └─┘     └─────┘
typ                                └───┘        └─┘    └─────┘        
doc                                                      └─────┘
 34    (h : ∀ n, n ∈ s → x * n * x⁻¹ ∈ s) : x ∈ is_subgroup.normalizer s :=
id                       └┘        └────────────────────┘ 
src                            └┘          └────────────────────┘
typ                      └┘        └────────────────────┘ 
 35  by haveI := classical.prop_decidable;
id               └──────────────────────┘
src     └───────┘└──────────────────────┘
typ     └───────┘└──────────────────────┘
doc     └───────┘
txt     └───────┘
par     └───────┘
pid          └─┘
st     └───────────────────────────────────
 36  haveI := set.fintype_image s (λ n, x * n * x⁻¹); exact
id            └───────────────┘               └┘
src  └───────┘└───────────────┘   └──┘    └┘  └────┘
typ  └───────┘└───────────────┘  └──┘   └┘  └────┘
doc  └───────┘                    └──┘         └────┘
txt  └───────┘                    └──┘         └────┘
par  └───────┘                    └──┘         └────┘
pid       └─┘                    └──┘              
st   ───────────────────────────────────────────────────────
 37  λ n, ⟨h n, λ h₁,
src   └──┘   └┘ └───┘
typ   └──┘   └┘ └───┘
doc   └──┘   └┘ └───┘
txt   └──┘   └┘ └───┘
par   └──┘   └┘ └───┘
pid   └──┘   └┘ └───┘
st   ─────────────────
 38  have heq : (λ n, x * n * x⁻¹) '' s = s := set.eq_of_subset_of_card_le
id                                 └┘         └─────────────────────────┘
src      └─────┘  └──┘       └┘└┘  └──┘└─────────────────────────┘
typ      └─────┘  └──┘       └┘└┘  └──┘└─────────────────────────┘
doc      └─────┘  └──┘       └┘     └──┘                           
txt      └─────┘  └──┘       └┘     └──┘                           
par      └─────┘  └──┘       └┘     └──┘                           
pid      └─────┘  └──┘       └┘     └──┘                           
st   ──────────────────────────────────────────────────────────────────────
 39    (λ n ⟨y, hy⟩, hy.2 ▸ h y hy.1) (by rw set.card_image_of_injective s conj_inj),
id             └┘                          └─────────────────────────┘  └──────┘
src  ─┘  └──┘ └┘  └─┘  └─┘     └──┘   └─┘└─────────────────────────┘ └──────┘└─┘
typ  ─┘  └──┘└┘└┘└─┘  └─┘    └──┘   └─┘└─────────────────────────┘└──────┘└─┘
doc  ─┘  └──┘ └┘  └─┘  └─┘     └──┘   └─┘                                    └─┘
txt  ─┘  └──┘ └┘  └─┘  └─┘     └──┘   └─┘                                    └─┘
par  ─┘  └──┘ └┘  └─┘  └─┘     └──┘   └─┘                                    └─┘
pid  ─┘  └──┘ └┘  └─┘  └─┘     └──┘   └──┘                                    └─┘
st   ───────────────────────────────────┘└────────────────────────────────────────┘└──
 40  have x * n * x⁻¹ ∈ (λ n, x * n * x⁻¹) '' s := heq.symm ▸ h₁,
id                                                 └───┘
src      └─┘        └──┘       └┘   └──┘   └───┘   └┘
typ      └─┘        └──┘      └┘  └──┘   └───┘   └┘
doc      └─┘         └──┘       └┘   └──┘           └┘
txt      └─┘         └──┘       └┘   └──┘           └┘
par      └─┘         └──┘       └┘   └──┘           └┘
pid      └─┘         └──┘       └┘   └──┘           └┘
st   ─────────────────────────────────────────────────────────────
 41  let ⟨y, hy⟩ := this in conj_inj hy.2 ▸ hy.1⟩
id           └┘                           
src       └┘  └───┘    └──┘          └─┘  └───
typ       └┘└┘└───┘    └──┘          └─┘  └───
doc       └┘  └───┘    └──┘          └─┘   └───
txt       └┘  └───┘    └──┘          └─┘   └───
par       └┘  └───┘    └──┘          └─┘   └───
pid       └┘  └───┘    └──┘          └─┘   └─┘
st   ─────────────────────────────────────────────
 42  
src  
typ  
doc  
txt  
par  
pid  
st   
 43  section order_of
 44  variables [group α] [fintype α] [decidable_eq α]
id              └───┘     └─────┘     └──────────┘
src             └───┘     └─────┘     └──────────┘
typ             └───┘     └─────┘     └──────────┘
doc                       └─────┘
 45  open quotient_group set
 46  
 47  instance quotient_group.fintype (s : set α) [is_subgroup s] [d : decidable_pred s] :
id                                        └─┘    └─────────┘        └────────────┘ 
src                                       └─┘     └─────────┘         └────────────┘
typ                                       └─┘    └─────────┘        └────────────┘ 
doc                                               └─────────┘
 48    fintype (quotient s) :=
id     └─────┘  └──────┘ 
src    └─────┘  └──────┘
typ    └─────┘  └──────┘ 
doc    └─────┘  └──────┘
 49  @quotient.fintype _ _ (left_rel s) (λ _ _, d _)
id    └──────────────┘      └──────┘         
src   └──────────────┘      └──────┘
typ   └──────────────┘      └──────┘         
 50  
 51  lemma card_eq_card_quotient_mul_card_subgroup (s : set α) [hs : is_subgroup s] [fintype s]
id                                                      └─┘         └─────────┘    └─────┘ 
src                                                     └─┘          └─────────┘     └─────┘
typ                                                     └─┘         └─────────┘    └─────┘ 
doc                                                                  └─────────┘     └─────┘
 52    [decidable_pred s] : fintype.card α = fintype.card (quotient s) * fintype.card s :=
id      └────────────┘     └──────────┘   └──────────┘  └──────┘    └──────────┘ 
src     └────────────┘      └──────────┘    └──────────┘  └──────┘     └──────────┘
typ     └────────────┘     └──────────┘   └──────────┘  └──────┘    └──────────┘ 
doc                         └──────────┘     └──────────┘  └──────┘      └──────────┘
 53  by rw ← fintype.card_prod;
id           └───────────────┘
src     └───┘└───────────────┘
typ     └───┘└───────────────┘
doc     └───┘
txt     └───┘
par     └───┘
pid       └─┘
st     └────────────────────────
 54    exact fintype.card_congr (is_subgroup.group_equiv_quotient_times_subgroup hs)
id           └────────────────┘  └─────────────────────────────────────────────┘ └┘
src    └────┘└────────────────┘ └─────────────────────────────────────────────┘  └─
typ    └────┘└────────────────┘ └─────────────────────────────────────────────┘└┘└─
doc    └────┘                                                                    └─
txt    └────┘                                                                    └─
par    └────┘                                                                    └─
pid                                                                             
st   ────────────────────────────────────────────────────────────────────────────────
 55  
src  
typ  
doc  
txt  
par  
pid  
st   
 56  lemma card_subgroup_dvd_card (s : set α) [is_subgroup s] [fintype s] :
id                                     └─┘    └─────────┘    └─────┘ 
src                                    └─┘     └─────────┘     └─────┘
typ                                    └─┘    └─────────┘    └─────┘ 
doc                                            └─────────┘     └─────┘
 57    fintype.card s ∣ fintype.card α :=
id     └──────────┘   └──────────┘ 
src    └──────────┘    └──────────┘
typ    └──────────┘   └──────────┘ 
doc    └──────────┘     └──────────┘
 58  by haveI := classical.prop_decidable; simp [card_eq_card_quotient_mul_card_subgroup s]
id               └──────────────────────┘        └─────────────────────────────────────┘ 
src     └───────┘└──────────────────────┘  └────┘└─────────────────────────────────────┘ └─
typ     └───────┘└──────────────────────┘  └────┘└─────────────────────────────────────┘└─
doc     └───────┘                          └────┘                                        └─
txt     └───────┘                          └────┘                                        └─
par     └───────┘                          └────┘                                        └─
pid          └─┘                                                                      
st     └────────────────────────────────────────────────────────────────────────────────────
 59  
src  
typ  
doc  
txt  
par  
pid  
st   
 60  lemma card_quotient_dvd_card (s : set α) [is_subgroup s] [decidable_pred s] [fintype s] :
id                                     └─┘    └─────────┘    └────────────┘    └─────┘ 
src                                    └─┘     └─────────┘     └────────────┘     └─────┘
typ                                    └─┘    └─────────┘    └────────────┘    └─────┘ 
doc                                            └─────────┘                        └─────┘
 61    fintype.card (quotient s) ∣ fintype.card α :=
id     └──────────┘  └──────┘    └──────────┘ 
src    └──────────┘  └──────┘     └──────────┘
typ    └──────────┘  └──────┘    └──────────┘ 
doc    └──────────┘  └──────┘      └──────────┘
 62  by simp [card_eq_card_quotient_mul_card_subgroup s]
id            └─────────────────────────────────────┘ 
src     └────┘└─────────────────────────────────────┘ └─
typ     └────┘└─────────────────────────────────────┘└─
doc     └────┘                                        └─
txt     └────┘                                        └─
par     └────┘                                        └─
pid                                                 
st     └─────────────────────────────────────────────────
 63  
src  
typ  
doc  
txt  
par  
pid  
st   
 64  @[simp] lemma card_trivial [fintype (is_subgroup.trivial α)] :
id                               └─────┘  └─────────────────┘ 
src                              └─────┘  └─────────────────┘
typ                              └─────┘  └─────────────────┘ 
doc    └──┘                      └─────┘  └─────────────────┘
 65    fintype.card (is_subgroup.trivial α) = 1 :=
id     └──────────┘  └─────────────────┘   
src    └──────────┘  └─────────────────┘    
typ    └──────────┘  └─────────────────┘   
doc    └──────────┘  └─────────────────┘
 66  fintype.card_eq_one_iff.2
id   └─────────────────────┘
src  └─────────────────────┘
typ  └─────────────────────┘
 67    ⟨⟨(1 : α), by simp⟩, λ ⟨y, hy⟩, subtype.eq $ is_subgroup.mem_trivial.1 hy⟩
id                              └┘   └────────┘   └─────────────────────┘
src                  └──┘              └────────┘   └─────────────────────┘
typ                 └──┘        └┘   └────────┘   └─────────────────────┘
doc                  └──┘
txt                  └──┘
par                  └──┘
st                  └───┘
 68  
 69  lemma exists_gpow_eq_one (a : α) : ∃i≠0, a ^ (i:ℤ) = 1 :=
id                                              
src                                                 
typ                                             
 70  have ¬ injective (λi:ℤ, a ^ i),
id         └───────┘         
src        └───────┘         
typ        └───────┘         
 71    from not_injective_infinite_fintype _,
id          └────────────────────────────┘
src         └────────────────────────────┘
typ         └────────────────────────────┘
 72  let ⟨i, j, a_eq, ne⟩ := show ∃(i j : ℤ), a ^ i = a ^ j ∧ i ≠ j,
id   └─┘            └┘                             
src                   └┘                                 
typ  └─┘            └┘                             
 73    by rw [injective] at this; simpa [classical.not_forall] in
id            └───────┘                  └──────────────────┘
src       └──┘└───────┘└───────┘  └─────┘└──────────────────┘└┘
typ       └──┘└───────┘└───────┘  └─────┘└──────────────────┘└┘
doc       └──┘         └───────┘  └─────┘                    └┘
txt       └──┘         └───────┘  └─────┘                    └┘
par       └──┘         └───────┘  └─────┘                    └┘
pid         └┘         └──────┘                           
st       └────────────┘└─────────────────────────────────────┘
 74  have a ^ (i - j) = 1,
id                 
src                 
typ                
 75    by simp [gpow_add, gpow_neg, a_eq],
id              └──────┘  └──────┘  └──┘
src       └────┘└──────┘└┘└──────┘└┘    
typ       └────┘└──────┘└┘└──────┘└┘└──┘
doc       └────┘        └┘        └┘    
txt       └────┘        └┘        └┘    
par       └────┘        └┘        └┘    
pid                   └┘        └┘    
st       └──────────────────────────────┘
 76  ⟨i - j, sub_ne_zero.mpr ne, this⟩
id          └─────────┘└──┘     └──┘
src         └─────────┘└──┘
typ         └─────────┘└──┘     └──┘
 77  
 78  lemma exists_pow_eq_one (a : α) : ∃i > 0, a ^ i = 1 :=
id                                            
src                                               
typ                                           
 79  let ⟨i, hi, eq⟩ := exists_gpow_eq_one a in
id   └─┘                └────────────────┘ 
src                     └────────────────┘
typ  └─┘                └────────────────┘ 
 80  begin
st   └─────
 81    cases i,
id           
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────┘└─
 82    { exact ⟨i, nat.pos_of_ne_zero (by simp [int.of_nat_eq_coe, *] at *), eq⟩ },
id                └────────────────┘           └───────────────┘            └┘
src      └────┘  └┘└────────────────┘   └────┘└───────────────┘└───────┘└─┘└┘└┘
typ      └────┘ └┘└────────────────┘   └────┘└───────────────┘└───────┘└─┘└┘└┘
doc      └────┘  └┘                     └────┘                 └───────┘└─┘  └┘
txt      └────┘  └┘                     └────┘                 └───────┘└─┘  └┘
par      └────┘  └┘                     └────┘                 └───────┘└─┘  └┘
pid             └┘                     └─────┘                 └──────────┘  
st   ───┘└──────────────────────────────┘└───────────────────────────────┘└─────┘└┘
 83    { exact ⟨i + 1, dec_trivial, inv_eq_one.1 eq⟩ }
id                   └─────────┘  └────────┘   └┘
src      └────┘  └──┘└─────────┘└┘└────────┘└─┘└┘└┘
typ      └────┘ └──┘└─────────┘└┘└────────┘└─┘└┘└┘
doc      └────┘   └──┘└─────────┘└┘          └─┘  └┘
txt      └────┘   └──┘           └┘          └─┘  └┘
par      └────┘   └──┘           └┘          └─┘  └┘
pid              └──┘           └┘          └─┘  
st   ───────────────────────────────────────────────┘└─
 84  end
st   ──┘
 85  
 86  /-- `order_of a` is the order of the element `a`, i.e. the `n ≥ 1`, s.t. `a ^ n = 1` -/
 87  def order_of (a : α) : ℕ := nat.find (exists_pow_eq_one a)
id                             └──────┘  └───────────────┘ 
src                             └──────┘  └───────────────┘
typ                            └──────┘  └───────────────┘ 
 88  
 89  lemma pow_order_of_eq_one (a : α) : a ^ order_of a = 1 :=
id                                        └──────┘  
src                                         └──────┘   
typ                                       └──────┘  
doc                                          └──────┘
 90  let ⟨h₁, h₂⟩ := nat.find_spec (exists_pow_eq_one a) in h₂
id   └─┘      └┘     └───────────┘  └───────────────┘ 
src                  └───────────┘  └───────────────┘
typ  └─┘      └┘     └───────────┘  └───────────────┘ 
 91  
 92  lemma order_of_pos (a : α) : order_of a > 0 :=
id                               └──────┘  
src                               └──────┘   
typ                              └──────┘  
doc                               └──────┘
 93  let ⟨h₁, h₂⟩ := nat.find_spec (exists_pow_eq_one a) in h₁
id   └─┘  └┘         └───────────┘  └───────────────┘ 
src                  └───────────┘  └───────────────┘
typ  └─┘  └┘         └───────────┘  └───────────────┘ 
 94  
 95  private lemma pow_injective_aux {n m : ℕ} (a : α) (h : n ≤ m)
id                                                          
src                                                          
typ                                                         
 96    (hn : n < order_of a) (hm : m < order_of a) (eq : a ^ n = a ^ m) : n = m :=
id             └──────┘           └──────┘                     
src             └──────┘             └──────┘                          
typ            └──────┘           └──────┘                     
doc              └──────┘              └──────┘
 97  decidable.by_contradiction $ assume ne : n ≠ m,
id   └────────────────────────┘                 
src  └────────────────────────┘                 
typ  └────────────────────────┘                 
 98    have h₁ : m - n > 0, from nat.pos_of_ne_zero (by simp [nat.sub_eq_iff_eq_add h, ne.symm]),
id                           └────────────────┘           └───────────────────┘ 
src                            └────────────────┘     └────┘└───────────────────┘ └┘       
typ                          └────────────────┘     └────┘└───────────────────┘└┘└─────┘
doc                                                     └────┘                      └┘       
txt                                                     └────┘                      └┘       
par                                                     └────┘                      └┘       
pid                                                                               └┘       
st                                                     └──────────────────────────────────────┘
 99    have h₂ : a ^ (m - n) = 1, by simp [pow_sub _ h, eq],
id                                   └─────┘     └┘
src                               └────┘└─────┘└─┘ └┘└┘
typ                            └────┘└─────┘└─┘└┘└┘
doc                                  └────┘       └─┘ └┘  
txt                                  └────┘       └─┘ └┘  
par                                  └────┘       └─┘ └┘  
pid                                             └─┘ └┘  
st                                  └─────────────────────┘
100    have le : order_of a ≤ m - n, from nat.find_min' (exists_pow_eq_one a) ⟨h₁, h₂⟩,
id               └──────┘            └───────────┘  └───────────────┘    └┘  └┘
src              └──────┘               └───────────┘  └───────────────┘
typ              └──────┘            └───────────┘  └───────────────┘    └┘  └┘
doc              └──────┘
101    have lt : m - n < order_of a,
id                   └──────┘ 
src                    └──────┘
typ                  └──────┘ 
doc                      └──────┘
102      from (nat.sub_lt_left_iff_lt_add h).mpr $ nat.lt_add_left _ _ _ hm,
id             └────────────────────────┘  └─┘    └─────────────┘       └┘
src            └────────────────────────┘   └─┘    └─────────────┘
typ            └────────────────────────┘  └─┘    └─────────────┘       └┘
103    lt_irrefl _ (lt_of_le_of_lt le lt)
id     └───────┘    └────────────┘ └┘ └┘
src    └───────┘    └────────────┘
typ    └───────┘    └────────────┘ └┘ └┘
104  
105  lemma pow_injective_of_lt_order_of {n m : ℕ} (a : α)
id                                                    
src                                            
typ                                                   
106    (hn : n < order_of a) (hm : m < order_of a) (eq : a ^ n = a ^ m) : n = m :=
id             └──────┘           └──────┘                     
src             └──────┘             └──────┘                          
typ            └──────┘           └──────┘                     
doc              └──────┘              └──────┘
107  (le_total n m).elim
id    └──────┘   └──┘
src   └──────┘     └──┘
typ   └──────┘   └──┘
108    (assume h, pow_injective_aux a h hn hm eq)
id               └───────────────┘   └┘ └┘ └┘
src               └───────────────┘           └┘
typ              └───────────────┘   └┘ └┘ └┘
109    (assume h, (pow_injective_aux a h hm hn eq.symm).symm)
id                └───────────────┘   └┘ └┘ └┘└───┘ └──┘
src                └───────────────┘           └┘└───┘ └──┘
typ               └───────────────┘   └┘ └┘ └┘└───┘ └──┘
110  
111  lemma order_of_le_card_univ : order_of a ≤ fintype.card α :=
id                                 └──────┘   └──────────┘ 
src                                └──────┘    └──────────┘
typ                                └──────┘   └──────────┘ 
doc                                └──────┘     └──────────┘
112  finset.card_le_of_inj_on ((^) a)
id   └──────────────────────┘     
src  └──────────────────────┘  
typ  └──────────────────────┘     
113    (assume n _, fintype.complete _)
id                └──────────────┘
src                 └──────────────┘
typ               └──────────────┘
114    (assume i j, pow_injective_of_lt_order_of a)
id                └──────────────────────────┘ 
src                 └──────────────────────────┘
typ               └──────────────────────────┘ 
115  
116  lemma pow_eq_mod_order_of {n : ℕ} : a ^ n = a ^ (n % order_of a) :=
id                                               └──────┘ 
src                                                  └──────┘
typ                                              └──────┘ 
doc                                                       └──────┘
117  calc a ^ n = a ^ (n % order_of a + order_of a * (n / order_of a)) :
id                  └──────┘   └──────┘      └──────┘ 
src                     └──────┘    └──────┘        └──────┘
typ                 └──────┘   └──────┘      └──────┘ 
doc                        └──────┘     └──────┘          └──────┘
118      by rw [nat.mod_add_div]
id              └─────────────┘
src         └──┘└─────────────┘└─
typ         └──┘└─────────────┘└─
doc         └──┘               └─
txt         └──┘               └─
par         └──┘               └─
pid           └┘               
st         └──────────────────┘
119    ... = a ^ (n % order_of a) :
id                └──────┘ 
src  ─┘             └──────┘
typ  ─┘           └──────┘ 
doc  ─┘               └──────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
120      by simp [pow_add, pow_mul, pow_order_of_eq_one]
id                └─────┘  └─────┘  └─────────────────┘
src         └────┘└─────┘└┘└─────┘└┘└─────────────────┘└─
typ         └────┘└─────┘└┘└─────┘└┘└─────────────────┘└─
doc         └────┘       └┘       └┘                   └─
txt         └────┘       └┘       └┘                   └─
par         └────┘       └┘       └┘                   └─
pid                    └┘       └┘                   
st         └─────────────────────────────────────────────
121  
src  
typ  
doc  
txt  
par  
pid  
st   
122  lemma gpow_eq_mod_order_of {i : ℤ} : a ^ i = a ^ (i % order_of a) :=
id                                                └──────┘ 
src                                                   └──────┘
typ                                               └──────┘ 
doc                                                        └──────┘
123  calc a ^ i = a ^ (i % order_of a + order_of a * (i / order_of a)) :
id                  └──────┘   └──────┘      └──────┘ 
src                     └──────┘    └──────┘        └──────┘
typ                 └──────┘   └──────┘      └──────┘ 
doc                        └──────┘     └──────┘          └──────┘
124      by rw [int.mod_add_div]
id              └─────────────┘
src         └──┘└─────────────┘└─
typ         └──┘└─────────────┘└─
doc         └──┘               └─
txt         └──┘               └─
par         └──┘               └─
pid           └┘               
st         └──────────────────┘
125    ... = a ^ (i % order_of a) :
id                └──────┘ 
src  ─┘             └──────┘
typ  ─┘           └──────┘ 
doc  ─┘               └──────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
126      by simp [gpow_add, gpow_mul, pow_order_of_eq_one]
id                └──────┘  └──────┘  └─────────────────┘
src         └────┘└──────┘└┘└──────┘└┘└─────────────────┘└─
typ         └────┘└──────┘└┘└──────┘└┘└─────────────────┘└─
doc         └────┘        └┘        └┘                   └─
txt         └────┘        └┘        └┘                   └─
par         └────┘        └┘        └┘                   └─
pid                     └┘        └┘                   
st         └───────────────────────────────────────────────
127  
src  
typ  
doc  
txt  
par  
pid  
st   
128  lemma mem_gpowers_iff_mem_range_order_of {a a' : α} :
id                                                    
typ                                                   
129    a' ∈ gpowers a ↔ a' ∈ (finset.range (order_of a)).image ((^) a : ℕ → α) :=
id     └┘  └─────┘   └┘   └──────────┘  └──────┘   └───┘            
src        └─────┘         └──────────┘  └──────┘    └───┘          
typ    └┘  └─────┘   └┘   └──────────┘  └──────┘   └───┘            
doc                           └──────────┘  └──────┘    └───┘
130  finset.mem_range_iff_mem_finset_range_of_mod_eq
id   └─────────────────────────────────────────────┘
src  └─────────────────────────────────────────────┘
typ  └─────────────────────────────────────────────┘
131    (order_of_pos a)
id      └──────────┘ 
src     └──────────┘
typ     └──────────┘ 
132    (assume i, gpow_eq_mod_order_of.symm)
id               └──────────────────┘└───┘
src               └──────────────────┘└───┘
typ              └──────────────────┘└───┘
133  
134  instance decidable_gpowers : decidable_pred (gpowers a) :=
id                                └────────────┘  └─────┘ 
src                               └────────────┘  └─────┘
typ                               └────────────┘  └─────┘ 
135  assume a', decidable_of_iff'
id          └┘  └───────────────┘
src             └───────────────┘
typ         └┘  └───────────────┘
136    (a' ∈ (finset.range (order_of a)).image ((^) a))
id      └┘   └──────────┘  └──────┘   └───┘      
src          └──────────┘  └──────┘    └───┘   
typ     └┘   └──────────┘  └──────┘   └───┘      
doc           └──────────┘  └──────┘    └───┘
137    mem_gpowers_iff_mem_range_order_of
id     └────────────────────────────────┘
src    └────────────────────────────────┘
typ    └────────────────────────────────┘
138  
139  lemma order_of_dvd_of_pow_eq_one {n : ℕ} (h : a ^ n = 1) : order_of a ∣ n :=
id                                                         └──────┘   
src                                                          └──────┘   
typ                                                        └──────┘   
doc                                                             └──────┘
140  by_contradiction
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
141    (λ h₁, nat.find_min _ (show n % order_of a < order_of a,
id        └┘  └──────────┘           └──────┘   └──────┘ 
src           └──────────┘            └──────┘    └──────┘
typ       └┘  └──────────┘           └──────┘   └──────┘ 
doc                                    └──────┘     └──────┘
142      from nat.mod_lt _ (order_of_pos _))
id            └────────┘    └──────────┘
src           └────────┘    └──────────┘
typ           └────────┘    └──────────┘
143        ⟨nat.pos_of_ne_zero (mt nat.dvd_of_mod_eq_zero h₁), by rwa ← pow_eq_mod_order_of⟩)
id          └────────────────┘  └┘ └────────────────────┘ └┘            └─────────────────┘
src         └────────────────┘  └┘ └────────────────────┘         └────┘└─────────────────┘
typ         └────────────────┘  └┘ └────────────────────┘ └┘      └────┘└─────────────────┘
doc                                                               └────┘
txt                                                               └────┘
par                                                               └────┘
pid                                                                  └─┘
st                                                               └────────────────────────┘
144  
145  lemma order_of_le_of_pow_eq_one {n : ℕ} (hn : 0 < n) (h : a ^ n = 1) : order_of a ≤ n :=
id                                                                   └──────┘   
src                                                                     └──────┘   
typ                                                                  └──────┘   
doc                                                                         └──────┘
146  nat.find_min' (exists_pow_eq_one a) ⟨hn, h⟩
id   └───────────┘  └───────────────┘    └┘  
src  └───────────┘  └───────────────┘
typ  └───────────┘  └───────────────┘    └┘  
147  
148  lemma sum_card_order_of_eq_card_pow_eq_one {n : ℕ} (hn : 0 < n) :
id                                                              
src                                                            
typ                                                             
149    ((finset.range n.succ).filter (∣ n)).sum (λ m, (finset.univ.filter (λ a : α, order_of a = m)).card)
id       └──────────┘ └───┘ └────┘      └─┘        └─────────┘└─────┘          └──────┘     └──┘
src      └──────────┘  └───┘ └────┘       └─┘         └─────────┘└─────┘           └──────┘       └──┘
typ      └──────────┘ └───┘ └────┘      └─┘        └─────────┘└─────┘          └──────┘     └──┘
doc      └──────────┘        └────┘                    └─────────┘└─────┘           └──────┘        └──┘
150    = (finset.univ.filter (λ a : α, a ^ n = 1)).card :=
id       └─────────┘└─────┘                 └──┘
src      └─────────┘└─────┘                    └──┘
typ      └─────────┘└─────┘                 └──┘
doc       └─────────┘└─────┘                      └──┘
151  calc ((finset.range n.succ).filter (∣ n)).sum (λ m, (finset.univ.filter (λ a : α, order_of a = m)).card)
id          └──────────┘ └───┘ └────┘      └─┘        └─────────┘└─────┘          └──────┘     └──┘
src         └──────────┘  └───┘ └────┘       └─┘         └─────────┘└─────┘           └──────┘       └──┘
typ         └──────────┘ └───┘ └────┘      └─┘        └─────────┘└─────┘          └──────┘     └──┘
doc         └──────────┘        └────┘                    └─────────┘└─────┘           └──────┘        └──┘
152      = _ : (finset.card_bind (by { intros, apply finset.disjoint_filter.2, cc })).symm
id              └──────────────┘                     └────────────────────┘          └──┘
src             └──────────────┘       └────┘  └────┘└────────────────────┘└┘  └─┘   └──┘
typ             └──────────────┘       └────┘  └────┘└────────────────────┘└┘  └─┘   └──┘
doc                                    └────┘  └────┘                      └┘  └─┘
txt                                    └────┘  └────┘                      └┘  └─┘
par                                    └────┘  └────┘                      └┘  └─┘
pid                                                                       └┘    
st                                  └───────┘└──────────────────────────────┘└───┘└┘
153  ... = _ : congr_arg finset.card (finset.ext.2 (begin
id             └───────┘ └─────────┘  └────────┘
src            └───────┘ └─────────┘  └────────┘
typ            └───────┘ └─────────┘  └────────┘
doc                      └─────────┘
st                                                  └─────
154    assume a,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
155    suffices : order_of a ≤ n ∧ order_of a ∣ n ↔ a ^ n = 1,
id                                └──────┘           
src    └─────────┘           └──────┘     └┘
typ    └─────────┘           └──────┘   └┘
doc    └─────────┘            └──────┘        └┘
txt    └─────────┘                            └┘
par    └─────────┘                            └┘
pid    └───────┘└┘                            
st   ───────────────────────────────────────────────────────┘└─
156    { simpa [nat.lt_succ_iff], },
id              └─────────────┘
src      └─────┘└─────────────┘
typ      └─────┘└─────────────┘
doc      └─────┘               
txt      └─────┘               
par      └─────┘               
pid                          
st   ───┘└─────────────────────┘└──┘
157    exact ⟨λ h, let ⟨m, hm⟩ := h.2 in by rw [hm, pow_mul, pow_order_of_eq_one, _root_.one_pow],
id                                              └┘  └─────┘  └─────────────────┘  └────────────┘
src    └────┘  └──┘     └┘  └───┘ └────┘  └──┘  └┘└─────┘└┘└─────────────────┘└┘└────────────┘└─
typ    └────┘  └──┘     └┘  └───┘ └────┘  └──┘└┘└┘└─────┘└┘└─────────────────┘└┘└────────────┘└─
doc    └────┘  └──┘     └┘  └───┘ └────┘  └──┘  └┘       └┘                   └┘              └─
txt    └────┘  └──┘     └┘  └───┘ └────┘  └──┘  └┘       └┘                   └┘              └─
par    └────┘  └──┘     └┘  └───┘ └────┘  └──┘  └┘       └┘                   └┘              └─
pid           └──┘     └┘  └───┘ └────┘  └───┘  └┘       └┘                   └┘              └──
st   ─────────────────────────────────────┘└─────┘└───────┘└───────────────────┘└──────────────┘└─
158      λ h, ⟨order_of_le_of_pow_eq_one hn h, order_of_dvd_of_pow_eq_one h⟩⟩
id             └───────────────────────┘ └┘    └────────────────────────┘
src  ───┘ └──┘ └───────────────────────┘   └┘└────────────────────────┘ └─┘
typ  ───┘ └──┘ └───────────────────────┘└┘ └┘└────────────────────────┘ └─┘
doc  ───┘ └──┘                             └┘                           └─┘
txt  ───┘ └──┘                             └┘                           └─┘
par  ───┘ └──┘                             └┘                           └─┘
pid  ───┘ └──┘                             └┘                           └┘
st   ────────────────────────────────────────────────────────────────────────┘
159  end))
st   └─┘
160  
161  section
162  local attribute [instance] set_fintype
id                              └─────────┘
src                             └─────────┘
typ                             └─────────┘
163  
164  lemma order_eq_card_gpowers : order_of a = fintype.card (gpowers a) :=
id                                 └──────┘   └──────────┘  └─────┘ 
src                                └──────┘    └──────────┘  └─────┘
typ                                └──────┘   └──────────┘  └─────┘ 
doc                                └──────┘     └──────────┘
165  begin
st   └─────
166    refine (finset.card_eq_of_bijective _ _ _ _).symm,
id             └─────────────────────────┘
src    └─────┘ └─────────────────────────┘└────────────┘
typ    └─────┘ └─────────────────────────┘└────────────┘
doc    └─────┘                            └────────────┘
txt    └─────┘                            └────────────┘
par    └─────┘                            └────────────┘
pid                                      └───────────┘
st   ──────────────────────────────────────────────────┘└─
167    { exact λn hn, ⟨gpow a n, ⟨n, rfl⟩⟩ },
id                     └──┘        └─┘
src      └────┘ └────┘ └──┘  └┘ └┘└─┘└─┘
typ      └────┘ └────┘ └──┘ └┘ └┘└─┘└─┘
doc      └────┘ └────┘ └──┘  └┘  └┘   └─┘
txt      └────┘ └────┘       └┘  └┘   └─┘
par      └────┘ └────┘       └┘  └┘   └─┘
pid            └────┘       └┘  └┘   └┘
st   ───┘└────────────────────────────────┘└┘
168    { exact assume ⟨_, i, rfl⟩ _,
id                        
src      └────┘      └───┘ └┘   └────
typ      └────┘      └───┘└┘   └────
doc      └────┘      └───┘ └┘   └────
txt      └────┘      └───┘ └┘   └────
par      └────┘      └───┘ └┘   └────
pid                 └───┘ └┘   └────
st   ───┘└───────────────────────────
169      have pos: (0:int) < order_of a,
id                    └─┘  
src  ───┘    └────┘ └┘└─┘└┘         └─
typ  ───┘    └────┘ └┘└─┘└┘         └─
doc  ───┘    └────┘ └┘   └┘          └─
txt  ───┘    └────┘ └┘   └┘          └─
par  ───┘    └────┘ └┘   └┘          └─
pid  ───┘    └────┘ └┘   └┘          └─
st   ────────────────────────────────────
170        from int.coe_nat_lt.mpr $ order_of_pos a,
id              └────────────────┘   └──────────┘ 
src  ──────────┘└────────────────┘ └──────────┘ └─
typ  ──────────┘└────────────────┘ └──────────┘└─
doc  ──────────┘                                └─
txt  ──────────┘                                └─
par  ──────────┘                                └─
pid  ──────────┘                                └─
st   ────────────────────────────────────────────────
171      have 0 ≤ i % (order_of a),
id                 
src  ───┘    └─┘           └──
typ  ───┘    └─┘           └──
doc  ───┘    └─┘             └──
txt  ───┘    └─┘             └──
par  ───┘    └─┘             └──
pid  ───┘    └─┘             └──
st   ───────────────────────────────
172        from int.mod_nonneg _ $ ne_of_gt pos,
id              └────────────┘     └──────┘
src  ──────────┘└────────────┘└─┘ └──────┘   └─
typ  ──────────┘└────────────┘└─┘ └──────┘   └─
doc  ──────────┘              └─┘            └─
txt  ──────────┘              └─┘            └─
par  ──────────┘              └─┘            └─
pid  ──────────┘              └─┘            └─
st   ────────────────────────────────────────────
173      ⟨int.to_nat (i % order_of a),
id        └────────┘      └──────┘
src  ───┘ └────────┘   └──────┘ └──
typ  ───┘ └────────┘   └──────┘ └──
doc  ───┘              └──────┘ └──
txt  ───┘                       └──
par  ───┘                       └──
pid  ───┘                       └──
st   ──────────────────────────────────
174        by rw [← int.coe_nat_lt, int.to_nat_of_nonneg this];
id                  └────────────┘  └──────────────────┘ └──┘
src  ─────┘  └────┘└────────────┘└┘└──────────────────┘    └─
typ  ─────┘  └────┘└────────────┘└┘└──────────────────┘└──┘└─
doc  ─────┘  └────┘              └┘                        └─
txt  ─────┘  └────┘              └┘                        └─
par  ─────┘  └────┘              └┘                        └─
pid  ─────┘  └─────┘              └┘                        └──
st   ───────┘└───────────────────┘└─────────────────────────┘└─
175          exact ⟨int.mod_lt_of_pos _ pos, subtype.eq gpow_eq_mod_order_of.symm⟩⟩ },
id                  └───────────────┘   └─┘  └────────┘ └───────────────────────┘
src  ─────────────┘ └───────────────┘└─┘└─┘└┘└────────┘└───────────────────────┘└─┘
typ  ─────────────┘ └───────────────┘└─┘└─┘└┘└────────┘└───────────────────────┘└─┘
doc  ─────────────┘                  └─┘   └┘                                   └─┘
txt  ─────────────┘                  └─┘   └┘                                   └─┘
par  ─────────────┘                  └─┘   └┘                                   └─┘
pid  ─────────────┘                  └─┘   └┘                                   └┘
st   ────────────────────────────────────────────────────────────────────────────┘└┘└┘
176    { intros, exact finset.mem_univ _ },
id                     └─────────────┘
src      └────┘  └────┘└─────────────┘└─┘
typ      └────┘  └────┘└─────────────┘└─┘
doc      └────┘  └────┘               └─┘
txt      └────┘  └────┘               └─┘
par      └────┘  └────┘               └─┘
pid                                  └┘
st   ───┘└────┘└────────────────────────┘└┘
177    { exact assume i j hi hj eq, pow_injective_of_lt_order_of a hi hj $ by simpa using eq }
id                                  └──────────────────────────┘                         └┘
src      └────┘      └─────────────┘└──────────────────────────┘        └──────────┘└┘
typ      └────┘      └─────────────┘└──────────────────────────┘       └──────────┘└┘
doc      └────┘      └─────────────┘                                    └──────────┘  
txt      └────┘      └─────────────┘                                    └──────────┘  
par      └────┘      └─────────────┘                                    └──────────┘  
pid                 └─────────────┘                                    └───────────┘  
st   ───────────────────────────────────────────────────────────────────────┘└──────────────┘└─
178  end
st   ──┘
179  
180  @[simp] lemma order_of_one : order_of (1 : α) = 1 :=
id                                └──────┘        
src                               └──────┘         
typ                               └──────┘        
doc    └──┘                       └──────┘
181  by rw [order_eq_card_gpowers, fintype.card_eq_one_iff];
id          └───────────────────┘  └─────────────────────┘
src     └──┘└───────────────────┘└┘└─────────────────────┘
typ     └──┘└───────────────────┘└┘└─────────────────────┘
doc     └──┘                     └┘                       
txt     └──┘                     └┘                       
par     └──┘                     └┘                       
pid       └┘                     └┘                       
st     └────────────────────────┘└───────────────────────┘└─
182    exact ⟨⟨1, 0, rfl⟩, λ ⟨a, i, ha⟩, by simp [ha.symm]⟩
id                   └─┘
src    └────┘  └────┘└─┘└─┘ └┘ └┘ └┘  └─┘  └────┘       └─
typ    └────┘  └────┘└─┘└─┘ └┘ └┘ └┘  └─┘  └────┘└─────┘└─
doc    └────┘  └────┘   └─┘ └┘ └┘ └┘  └─┘  └────┘       └─
txt    └────┘  └────┘   └─┘ └┘ └┘ └┘  └─┘  └────┘       └─
par    └────┘  └────┘   └─┘ └┘ └┘ └┘  └─┘  └────┘       └─
pid           └────┘   └─┘ └┘ └┘ └┘  └─┘  └─────┘       └┘
st   ─────────────────────────────────────┘└─────────────┘└─
183  
src  
typ  
doc  
txt  
par  
pid  
st   
184  @[simp] lemma order_of_eq_one_iff : order_of a = 1 ↔ a = 1 :=
id                                       └──────┘       
src                                      └──────┘         
typ                                      └──────┘       
doc    └──┘                              └──────┘
185  ⟨λ h, by conv { to_lhs, rw [← pow_one a, ← h, pow_order_of_eq_one] }, λ h, by simp [h]⟩
id                                └─────┘       └─────────────────┘                  
src           └─────┘└────┘└┘└────┘└─────┘ └──┘ └┘└─────────────────┘└┘          └────┘ 
typ          └─────┘└────┘└┘└────┘└─────┘└──┘└┘└─────────────────┘└┘         └────┘
doc                                                                                └────┘ 
txt           └─────┘└────┘└┘└────┘        └──┘ └┘                   └┘          └────┘ 
par           └─────┘└────┘└┘└────┘        └──┘ └┘                   └┘          └────┘ 
pid               └──────────────┘        └──┘ └┘                   └─┘               
st           └─────┘└─────┘└───────────────┘└───┘└───────────────────┘ └┘        └───────┘
186  
187  section classical
188  open_locale classical
189  open quotient_group
190  
191  /- TODO: use cardinal theory, introduce `card : set α → ℕ`, or setup decidability for cosets -/
192  lemma order_of_dvd_card_univ : order_of a ∣ fintype.card α :=
id                                  └──────┘   └──────────┘ 
src                                 └──────┘    └──────────┘
typ                                 └──────┘   └──────────┘ 
doc                                 └──────┘     └──────────┘
193  have ft_prod : fintype (quotient (gpowers a) × (gpowers a)),
id                  └─────┘  └──────┘  └─────┘     └─────┘ 
src                 └─────┘  └──────┘  └─────┘      └─────┘
typ                 └─────┘  └──────┘  └─────┘     └─────┘ 
doc                 └─────┘  └──────┘
194    from fintype.of_equiv α (gpowers.is_subgroup a).group_equiv_quotient_times_subgroup,
id          └──────────────┘   └─────────────────┘  └─────────────────────────────────┘
src         └──────────────┘    └─────────────────┘   └─────────────────────────────────┘
typ         └──────────────┘   └─────────────────┘  └─────────────────────────────────┘
doc         └──────────────┘
195  have ft_s : fintype (gpowers a),
id               └─────┘  └─────┘ 
src              └─────┘  └─────┘
typ              └─────┘  └─────┘ 
doc              └─────┘
196    from @fintype.fintype_prod_right _ _ _ ft_prod _,
id           └────────────────────────┘       └─────┘
src          └────────────────────────┘
typ          └────────────────────────┘       └─────┘
197  have ft_cosets : fintype (quotient (gpowers a)),
id                    └─────┘  └──────┘  └─────┘ 
src                   └─────┘  └──────┘  └─────┘
typ                   └─────┘  └──────┘  └─────┘ 
doc                   └─────┘  └──────┘
198    from @fintype.fintype_prod_left _ _ _ ft_prod ⟨⟨1, is_submonoid.one_mem (gpowers a)⟩⟩,
id           └───────────────────────┘       └─────┘      └──────────────────┘  └─────┘ 
src          └───────────────────────┘                    └──────────────────┘  └─────┘
typ          └───────────────────────┘       └─────┘      └──────────────────┘  └─────┘ 
199  have ft : fintype (quotient (gpowers a) × (gpowers a)),
id             └─────┘  └──────┘  └─────┘     └─────┘ 
src            └─────┘  └──────┘  └─────┘      └─────┘
typ            └─────┘  └──────┘  └─────┘     └─────┘ 
doc            └─────┘  └──────┘
200    from @prod.fintype _ _ ft_cosets ft_s,
id           └──────────┘     └───────┘ └──┘
src          └──────────┘
typ          └──────────┘     └───────┘ └──┘
201  have eq₁ : fintype.card α = @fintype.card _ ft_cosets * @fintype.card _ ft_s,
id              └──────────┘    └──────────┘   └───────┘   └──────────┘   └──┘
src             └──────────┘     └──────────┘               └──────────┘
typ             └──────────┘    └──────────┘   └───────┘   └──────────┘   └──┘
doc             └──────────┘      └──────────┘                └──────────┘
202    from calc fintype.card α = @fintype.card _ ft_prod :
id               └──────────┘     └──────────┘   └─────┘
src              └──────────┘      └──────────┘
typ              └──────────┘     └──────────┘   └─────┘
doc              └──────────┘      └──────────┘
203        @fintype.card_congr _ _ _ ft_prod (gpowers.is_subgroup a).group_equiv_quotient_times_subgroup
id          └────────────────┘       └─────┘  └─────────────────┘  └─────────────────────────────────┘
src         └────────────────┘                └─────────────────┘   └─────────────────────────────────┘
typ         └────────────────┘       └─────┘  └─────────────────┘  └─────────────────────────────────┘
204      ... = @fintype.card _ (@prod.fintype _ _ ft_cosets ft_s) :
id              └──────────┘     └──────────┘     └───────┘ └──┘
src             └──────────┘     └──────────┘
typ             └──────────┘     └──────────┘     └───────┘ └──┘
doc             └──────────┘
205        congr_arg (@fintype.card _) $ subsingleton.elim _ _
id         └───────┘   └──────────┘      └───────────────┘
src        └───────┘   └──────────┘      └───────────────┘
typ        └───────┘   └──────────┘      └───────────────┘
doc                    └──────────┘
206      ... = @fintype.card _ ft_cosets * @fintype.card _ ft_s :
id              └──────────┘   └───────┘   └──────────┘   └──┘
src             └──────────┘               └──────────┘
typ             └──────────┘   └───────┘   └──────────┘   └──┘
doc             └──────────┘                └──────────┘
207        @fintype.card_prod _ _ ft_cosets ft_s,
id          └───────────────┘     └───────┘ └──┘
src         └───────────────┘
typ         └───────────────┘     └───────┘ └──┘
208  have eq₂ : order_of a = @fintype.card _ ft_s,
id              └──────┘    └──────────┘   └──┘
src             └──────┘     └──────────┘
typ             └──────┘    └──────────┘   └──┘
doc             └──────┘      └──────────┘
209    from calc order_of a = _ : order_eq_card_gpowers
id               └──────┘        └───────────────────┘
src              └──────┘         └───────────────────┘
typ              └──────┘        └───────────────────┘
doc              └──────┘
210      ... = _ : congr_arg (@fintype.card _) $ subsingleton.elim _ _,
id                 └───────┘   └──────────┘      └───────────────┘
src                └───────┘   └──────────┘      └───────────────┘
typ                └───────┘   └──────────┘      └───────────────┘
doc                            └──────────┘
211  dvd.intro (@fintype.card (quotient (gpowers a)) ft_cosets) $
id   └───────┘   └──────────┘  └──────┘  └─────┘    └───────┘
src  └───────┘   └──────────┘  └──────┘  └─────┘
typ  └───────┘   └──────────┘  └──────┘  └─────┘    └───────┘
doc              └──────────┘  └──────┘
212    by rw [eq₁, eq₂, mul_comm]
id            └─┘  └─┘  └──────┘
src       └──┘   └┘   └┘└──────┘└─
typ       └──┘└─┘└┘└─┘└┘└──────┘└─
doc       └──┘   └┘   └┘        └─
txt       └──┘   └┘   └┘        └─
par       └──┘   └┘   └┘        └─
pid         └┘   └┘   └┘        
st       └──────┘└───┘└────────┘
213  
src  
typ  
doc  
txt  
par  
pid  
st   
214  
src  
typ  
doc  
txt  
par  
pid  
st   
215  end classical
216  
217  @[simp] lemma pow_card_eq_one (a : α) : a ^ fintype.card α = 1 :=
id                                            └──────────┘  
src                                             └──────────┘   
typ                                           └──────────┘  
doc    └──┘                                      └──────────┘
218  let ⟨m, hm⟩ := @order_of_dvd_card_univ _ a _ _ _ in
id   └─┘             └────────────────────┘   
src                  └────────────────────┘
typ  └─┘             └────────────────────┘   
219  by simp [hm, pow_mul, pow_order_of_eq_one]
id            └┘  └─────┘  └─────────────────┘
src     └────┘  └┘└─────┘└┘└─────────────────┘└─
typ     └────┘└┘└┘└─────┘└┘└─────────────────┘└─
doc     └────┘  └┘       └┘                   └─
txt     └────┘  └┘       └┘                   └─
par     └────┘  └┘       └┘                   └─
pid           └┘       └┘                   
st     └────────────────────────────────────────
220  
src  
typ  
doc  
txt  
par  
pid  
st   
221  lemma powers_eq_gpowers (a : α) : powers a = gpowers a :=
id                                    └────┘   └─────┘ 
src                                    └────┘    └─────┘
typ                                   └────┘   └─────┘ 
doc                                    └────┘
222  set.ext (λ x, ⟨λ ⟨n, hn⟩, ⟨n, by simp * at *⟩,
id   └─────┘         
src  └─────┘                          └─────────┘
typ  └─────┘                       └─────────┘
doc                                   └─────────┘
txt                                   └─────────┘
par                                   └─────────┘
pid                                       └──┘
st                                   └──────────┘
223    λ ⟨i, hi⟩, ⟨(i % order_of a).nat_abs,
id                   └──────┘  └─────┘
src                    └──────┘   └─────┘
typ                  └──────┘  └─────┘
doc                     └──────┘
224      by rwa [← gpow_coe_nat, int.nat_abs_of_nonneg (int.mod_nonneg _
id                 └──────────┘  └───────────────────┘  └────────────┘
src         └─────┘└──────────┘└┘└───────────────────┘ └────────────┘└──
typ         └─────┘└──────────┘└┘└───────────────────┘ └────────────┘└──
doc         └─────┘            └┘                                    └──
txt         └─────┘            └┘                                    └──
par         └─────┘            └┘                                    └──
pid            └──┘            └┘                                    └──
st         └──────────────────┘└─────────────────────────────────────────
225        (int.coe_nat_ne_zero_iff_pos.2 (order_of_pos _))), ← gpow_eq_mod_order_of]⟩⟩)
id          └─────────────────────────┘    └──────────┘         └──────────────────┘
src  ─────┘ └─────────────────────────┘└─┘ └──────────┘└───────┘└──────────────────┘
typ  ─────┘ └─────────────────────────┘└─┘ └──────────┘└───────┘└──────────────────┘
doc  ─────┘                            └─┘             └───────┘                    
txt  ─────┘                            └─┘             └───────┘                    
par  ─────┘                            └─┘             └───────┘                    
pid  ─────┘                            └─┘             └───────┘                    
st   ──────────────────────────────────────────────────────┘└──────────────────────┘
226  
227  open nat
228  
229  lemma order_of_pow (a : α) (n : ℕ) : order_of (a ^ n) = order_of a / gcd (order_of a) n :=
id                                      └──────┘       └──────┘   └─┘  └──────┘   
src                                      └──────┘         └──────┘    └─┘  └──────┘
typ                                     └──────┘       └──────┘   └─┘  └──────┘   
doc                                       └──────┘           └──────┘          └──────┘
230  dvd_antisymm
id   └──────────┘
src  └──────────┘
typ  └──────────┘
231    (order_of_dvd_of_pow_eq_one
id      └────────────────────────┘
src     └────────────────────────┘
typ     └────────────────────────┘
232      (by rw [← pow_mul, ← nat.mul_div_assoc _ (gcd_dvd_left _ _), mul_comm,
id                 └─────┘    └───────────────┘    └──────────┘       └──────┘
src          └────┘└─────┘└──┘└───────────────┘└─┘ └──────────┘└─────┘└──────┘└─
typ          └────┘└─────┘└──┘└───────────────┘└─┘ └──────────┘└─────┘└──────┘└─
doc          └────┘       └──┘                 └─┘             └─────┘        └─
txt          └────┘       └──┘                 └─┘             └─────┘        └─
par          └────┘       └──┘                 └─┘             └─────┘        └─
pid            └──┘       └──┘                 └─┘             └─────┘        └─
st          └────────────┘└────────────────────────────────────────┘└────────┘└─
233        nat.mul_div_assoc _ (gcd_dvd_right _ _), pow_mul, pow_order_of_eq_one, _root_.one_pow]))
id         └───────────────┘    └───────────┘       └─────┘  └─────────────────┘  └────────────┘
src  ─────┘└───────────────┘└─┘ └───────────┘└─────┘└─────┘└┘└─────────────────┘└┘└────────────┘
typ  ─────┘└───────────────┘└─┘ └───────────┘└─────┘└─────┘└┘└─────────────────┘└┘└────────────┘
doc  ─────┘                 └─┘              └─────┘       └┘                   └┘              
txt  ─────┘                 └─┘              └─────┘       └┘                   └┘              
par  ─────┘                 └─┘              └─────┘       └┘                   └┘              
pid  ─────┘                 └─┘              └─────┘       └┘                   └┘              
st   ────────────────────────────────────────────┘└───────┘└───────────────────┘└──────────────┘
234    (have gcd_pos : 0 < gcd (order_of a) n, from gcd_pos_of_pos_left n (order_of_pos a),
id                        └─┘  └──────┘          └─────────────────┘   └──────────┘ 
src                       └─┘  └──────┘            └─────────────────┘    └──────────┘
typ                       └─┘  └──────┘          └─────────────────┘   └──────────┘ 
doc                             └──────┘
235      have hdvd : order_of a ∣ n * order_of (a ^ n),
id                   └──────┘     └──────┘    
src                  └──────┘       └──────┘    
typ                  └──────┘     └──────┘    
doc                  └──────┘         └──────┘
236        from order_of_dvd_of_pow_eq_one (by rw [pow_mul, pow_order_of_eq_one]),
id              └────────────────────────┘         └─────┘  └─────────────────┘
src             └────────────────────────┘     └──┘└─────┘└┘└─────────────────┘
typ             └────────────────────────┘     └──┘└─────┘└┘└─────────────────┘
doc                                            └──┘       └┘                   
txt                                            └──┘       └┘                   
par                                            └──┘       └┘                   
pid                                              └┘       └┘                   
st                                            └──────────┘└───────────────────┘
237      coprime.dvd_of_dvd_mul_right (coprime_div_gcd_div_gcd gcd_pos)
id       └──────────────────────────┘  └─────────────────────┘ └─────┘
src      └──────────────────────────┘  └─────────────────────┘
typ      └──────────────────────────┘  └─────────────────────┘ └─────┘
238        (dvd_of_mul_dvd_mul_right gcd_pos
id          └──────────────────────┘ └─────┘
src         └──────────────────────┘
typ         └──────────────────────┘ └─────┘
239          (by rwa [nat.div_mul_cancel (gcd_dvd_left _ _), mul_assoc,
id                    └────────────────┘  └──────────┘       └───────┘
src              └───┘└────────────────┘ └──────────┘└─────┘└───────┘└─
typ              └───┘└────────────────┘ └──────────┘└─────┘└───────┘└─
doc              └───┘                               └─────┘         └─
txt              └───┘                               └─────┘         └─
par              └───┘                               └─────┘         └─
pid                 └┘                               └─────┘         └─
st              └─────────────────────────────────────────┘└─────────┘└─
240              nat.div_mul_cancel (gcd_dvd_right _ _), mul_comm])))
id               └────────────────┘  └───────────┘       └──────┘
src  ───────────┘└────────────────┘ └───────────┘└─────┘└──────┘
typ  ───────────┘└────────────────┘ └───────────┘└─────┘└──────┘
doc  ───────────┘                                └─────┘        
txt  ───────────┘                                └─────┘        
par  ───────────┘                                └─────┘        
pid  ───────────┘                                └─────┘        
st   ─────────────────────────────────────────────────┘└────────┘
241  
242  lemma pow_gcd_card_eq_one_iff {n : ℕ} {a : α} :
id                                             
src                                     
typ                                            
243    a ^ n = 1 ↔ a ^ (gcd n (fintype.card α)) = 1 :=
id               └─┘   └──────────┘    
src                 └─┘    └──────────┘     
typ              └─┘   └──────────┘    
doc                            └──────────┘
244  ⟨λ h, have hn : order_of a ∣ n, from dvd_of_mod_eq_zero $
id                  └──────┘          └────────────────┘
src                  └──────┘            └────────────────┘
typ                 └──────┘          └────────────────┘
doc                  └──────┘
245        by_contradiction (λ ha, by rw pow_eq_mod_order_of at h;
id         └──────────────┘    └┘        └─────────────────┘
src        └──────────────┘           └─┘└─────────────────┘└───┘
typ        └──────────────┘    └┘     └─┘└─────────────────┘└───┘
doc                                   └─┘                   └───┘
txt                                   └─┘                   └───┘
par                                   └─┘                   └───┘
pid                                                        └───┘
st                                   └─────────────────────────────
246          exact (not_le_of_gt (nat.mod_lt n (order_of_pos a)))
id                  └──────────┘  └────────┘   └──────────┘ 
src          └────┘ └──────────┘ └────────┘  └──────────┘ └───
typ          └────┘ └──────────┘ └────────┘ └──────────┘└───
doc          └────┘                                       └───
txt          └────┘                                       └───
par          └────┘                                       └───
pid                                                      └───
st   ─────────────────────────────────────────────────────────────
247            (order_of_le_of_pow_eq_one (nat.pos_of_ne_zero ha) h)),
id              └───────────────────────┘  └────────────────┘ └┘  
src  ─────────┘ └───────────────────────┘ └────────────────┘  └┘ 
typ  ─────────┘ └───────────────────────┘ └────────────────┘└┘└┘
doc  ─────────┘                                               └┘ 
txt  ─────────┘                                               └┘ 
par  ─────────┘                                               └┘ 
pid  ─────────┘                                               └┘ 
st   ──────────────────────────────────────────────────────────────┘
248      let ⟨m, hm⟩ := dvd_gcd hn order_of_dvd_card_univ in
id       └─┘            └─────┘ └┘ └────────────────────┘
src                     └─────┘    └────────────────────┘
typ      └─┘            └─────┘ └┘ └────────────────────┘
249      by rw [hm, pow_mul, pow_order_of_eq_one, _root_.one_pow],
id              └┘  └─────┘  └─────────────────┘  └────────────┘
src         └──┘  └┘└─────┘└┘└─────────────────┘└┘└────────────┘
typ         └──┘└┘└┘└─────┘└┘└─────────────────┘└┘└────────────┘
doc         └──┘  └┘       └┘                   └┘              
txt         └──┘  └┘       └┘                   └┘              
par         └──┘  └┘       └┘                   └┘              
pid           └┘  └┘       └┘                   └┘              
st         └─────┘└───────┘└───────────────────┘└──────────────┘
250    λ h, let ⟨m, hm⟩ := gcd_dvd_left n (fintype.card α) in
id         └─┘            └──────────┘   └──────────┘ 
src                        └──────────┘    └──────────┘
typ        └─┘            └──────────┘   └──────────┘ 
doc                                        └──────────┘
251      by rw [hm, pow_mul, h, _root_.one_pow]⟩
id              └┘  └─────┘    └────────────┘
src         └──┘  └┘└─────┘└┘ └┘└────────────┘
typ         └──┘└┘└┘└─────┘└┘└┘└────────────┘
doc         └──┘  └┘       └┘ └┘              
txt         └──┘  └┘       └┘ └┘              
par         └──┘  └┘       └┘ └┘              
pid           └┘  └┘       └┘ └┘              
st         └─────┘└───────┘└─┘└──────────────┘
252  
253  end
254  
255  end order_of
256  
257  section cyclic
258  
259  local attribute [instance] set_fintype
id                              └─────────┘
src                             └─────────┘
typ                             └─────────┘
260  
261  class is_cyclic (α : Type*) [group α] : Prop :=
id                        └───┘   └───┘ 
src                               └───┘
typ                       └───┘   └───┘ 
262  (exists_generator : ∃ g : α, ∀ x, x ∈ gpowers g)
id                                   └─────┘ 
src                                     └─────┘
typ                                  └─────┘ 
263  
264  def is_cyclic.comm_group [hg : group α] [is_cyclic α] : comm_group α :=
id                                  └───┘    └───────┘     └────────┘ 
src                                 └───┘     └───────┘      └────────┘
typ                                 └───┘    └───────┘     └────────┘ 
265  { mul_comm := λ x y, show x * y = y * x,
id                                 
src                                    
typ                                
266      from let ⟨g, hg⟩ := is_cyclic.exists_generator α in
id            └─┘     └┘     └────────────────────────┘ 
src                          └────────────────────────┘
typ           └─┘     └┘     └────────────────────────┘ 
267      let ⟨n, hn⟩ := hg x in let ⟨m, hm⟩ := hg y in
id       └─┘     └┘            └─┘     └┘        
typ      └─┘     └┘            └─┘     └┘        
268      hm ▸ hn ▸ gpow_mul_comm _ _ _,
id               └───────────┘
src              └───────────┘
typ              └───────────┘
269    ..hg }
id       └┘
typ      └┘
270  
271  lemma is_cyclic_of_order_of_eq_card [group α] [fintype α] [decidable_eq α]
id                                        └───┘    └─────┘    └──────────┘ 
src                                       └───┘     └─────┘     └──────────┘
typ                                       └───┘    └─────┘    └──────────┘ 
doc                                                 └─────┘
272    (x : α) (hx : order_of x = fintype.card α) : is_cyclic α :=
id                  └──────┘   └──────────┘     └───────┘ 
src                  └──────┘    └──────────┘      └───────┘
typ                 └──────┘   └──────────┘     └───────┘ 
doc                  └──────┘     └──────────┘
273  ⟨⟨x, set.eq_univ_iff_forall.1 $ set.eq_of_subset_of_card_le
id       └────────────────────┘    └─────────────────────────┘
src       └────────────────────┘    └─────────────────────────┘
typ      └────────────────────┘    └─────────────────────────┘
274    (set.subset_univ _)
id      └─────────────┘
src     └─────────────┘
typ     └─────────────┘
275    (by rw [fintype.card_congr (equiv.set.univ α), ← hx, order_eq_card_gpowers])⟩⟩
id             └────────────────┘  └────────────┘      └┘  └───────────────────┘
src        └──┘└────────────────┘ └────────────┘ └───┘  └┘└───────────────────┘
typ        └──┘└────────────────┘ └────────────┘└───┘└┘└┘└───────────────────┘
doc        └──┘                                  └───┘  └┘                     
txt        └──┘                                  └───┘  └┘                     
par        └──┘                                  └───┘  └┘                     
pid          └┘                                  └───┘  └┘                     
st        └────────────────────────────────────────┘└────┘└─────────────────────┘
276  
277  lemma order_of_eq_card_of_forall_mem_gpowers [group α] [fintype α] [decidable_eq α]
id                                                 └───┘    └─────┘    └──────────┘ 
src                                                └───┘     └─────┘     └──────────┘
typ                                                └───┘    └─────┘    └──────────┘ 
doc                                                          └─────┘
278    {g : α} (hx : ∀ x, x ∈ gpowers g) : order_of g = fintype.card α :=
id                        └─────┘     └──────┘   └──────────┘ 
src                          └─────┘      └──────┘    └──────────┘
typ                       └─────┘     └──────┘   └──────────┘ 
doc                                        └──────┘     └──────────┘
279  by rw [← fintype.card_congr (equiv.set.univ α), order_eq_card_gpowers];
id            └────────────────┘  └────────────┘    └───────────────────┘
src     └────┘└────────────────┘ └────────────┘ └─┘└───────────────────┘
typ     └────┘└────────────────┘ └────────────┘└─┘└───────────────────┘
doc     └────┘                                  └─┘                     
txt     └────┘                                  └─┘                     
par     └────┘                                  └─┘                     
pid       └──┘                                  └─┘                     
st     └──────────────────────────────────────────┘└─────────────────────┘└─
280    simp [hx]; congr
id           └┘
src    └────┘    └─────
typ    └────┘└┘  └─────
doc    └────┘  
txt    └────┘    └─────
par    └────┘    └─────
pid                 
st   ───────────────────
281  
src  
typ  
txt  
par  
pid  
st   
282  instance [group α] : is_cyclic (is_subgroup.trivial α) :=
id             └───┘     └───────┘  └─────────────────┘ 
src            └───┘      └───────┘  └─────────────────┘
typ            └───┘     └───────┘  └─────────────────┘ 
doc                                  └─────────────────┘
283  ⟨⟨(1 : is_subgroup.trivial α), λ x, ⟨0, subtype.eq $ eq.symm (is_subgroup.mem_trivial.1 x.2)⟩⟩⟩
id          └─────────────────┘            └────────┘   └─────┘  └─────────────────────┘  
src         └─────────────────┘              └────────┘   └─────┘  └─────────────────────┘   
typ         └─────────────────┘            └────────┘   └─────┘  └─────────────────────┘  
doc         └─────────────────┘
284  
285  instance is_subgroup.is_cyclic [group α] [is_cyclic α] (H : set α) [is_subgroup H] : is_cyclic H :=
id                                   └───┘    └───────┘        └─┘    └─────────┘     └───────┘ 
src                                  └───┘     └───────┘         └─┘     └─────────┘      └───────┘
typ                                  └───┘    └───────┘        └─┘    └─────────┘     └───────┘ 
doc                                                                      └─────────┘
286  by haveI := classical.prop_decidable; exact
id               └──────────────────────┘
src     └───────┘└──────────────────────┘  └────┘
typ     └───────┘└──────────────────────┘  └────┘
doc     └───────┘                          └────┘
txt     └───────┘                          └────┘
par     └───────┘                          └────┘
pid          └─┘                               
st     └─────────────────────────────────────────
287  let ⟨g, hg⟩ := is_cyclic.exists_generator α in
id          └┘     └────────────────────────┘ 
src       └┘  └───┘└────────────────────────┘ └──┘
typ      └┘└┘└───┘└────────────────────────┘└──┘
doc       └┘  └───┘                           └──┘
txt       └┘  └───┘                           └──┘
par       └┘  └───┘                           └──┘
pid       └┘  └───┘                           └──┘
st   ───────────────────────────────────────────────
288  if hx : ∃ (x : α), x ∈ H ∧ x ≠ (1 : α) then
id   └┘                       
src  └┘└────┘└────┘     └──┘ └──────
typ  └┘└────┘└────┘     └──┘ └──────
doc    └────┘ └────┘         └──┘ └──────
txt    └────┘ └────┘         └──┘ └──────
par    └────┘ └────┘         └──┘ └──────
pid    └────┘ └────┘         └──┘ └──────
st   ────────────────────────────────────────────
289    let ⟨x, hx₁, hx₂⟩ := hx in
id                 └─┘
src  ─┘     └┘   └┘   └───┘  └───
typ  ─┘    └┘   └┘└─┘└───┘  └───
doc  ─┘     └┘   └┘   └───┘  └───
txt  ─┘     └┘   └┘   └───┘  └───
par  ─┘     └┘   └┘   └───┘  └───
pid  ─┘     └┘   └┘   └───┘  └───
st   ─────────────────────────────
290    let ⟨k, hk⟩ := hg x in
id            └┘
src  ─┘     └┘  └───┘   └───
typ  ─┘    └┘└┘└───┘   └───
doc  ─┘     └┘  └───┘   └───
txt  ─┘     └┘  └───┘   └───
par  ─┘     └┘  └───┘   └───
pid  ─┘     └┘  └───┘   └───
st   ─────────────────────────
291    have hex : ∃ n : ℕ, 0 < n ∧ g ^ n ∈ H,
id                                 
src  ─┘    └─────┘ └───┘  └─┘      └─
typ  ─┘    └─────┘ └───┘  └─┘     └─
doc  ─┘    └─────┘ └───┘  └─┘        └─
txt  ─┘    └─────┘ └───┘  └─┘        └─
par  ─┘    └─────┘ └───┘  └─┘        └─
pid  ─┘    └─────┘ └───┘  └─┘        └─
st   ─────────────────────────────────────────
292      from ⟨k.nat_abs, nat.pos_of_ne_zero
id              └──────┘  └────────────────┘
src  ────────┘  └──────┘└┘└────────────────┘
typ  ────────┘  └──────┘└┘└────────────────┘
doc  ────────┘          └┘                  
txt  ────────┘          └┘                  
par  ────────┘          └┘                  
pid  ────────┘          └┘                  
st   ────────────────────────────────────────
293        (λ h, hx₂ $ by rw [← hk, int.eq_zero_of_nat_abs_eq_zero h, gpow_zero]),
id                              └┘  └────────────────────────────┘   └───────┘
src  ─────┘  └──┘      └────┘  └┘└────────────────────────────┘ └┘└───────┘└──
typ  ─────┘  └──┘      └────┘└┘└┘└────────────────────────────┘└┘└───────┘└──
doc  ─────┘  └──┘      └────┘  └┘                               └┘         └──
txt  ─────┘  └──┘      └────┘  └┘                               └┘         └──
par  ─────┘  └──┘      └────┘  └┘                               └┘         └──
pid  ─────┘  └──┘      └─────┘  └┘                               └┘         └───
st   ───────────────────┘└───────┘└────────────────────────────────┘└─────────┘└──
294          match k, hk with
src  ───────┘      └┘  └─────
typ  ───────┘      └┘  └─────
doc  ───────┘      └┘  └─────
txt  ───────┘      └┘  └─────
par  ───────┘      └┘  └─────
pid  ───────┘      └┘  └─────
st   ─────────────────────────
295          | (k : ℕ), hk := by rw [int.nat_abs_of_nat, ← gpow_coe_nat, hk]; exact hx₁
id                                   └────────────────┘    └──────────┘  └┘         └─┘
src  ─────────┘  └─┘ └─┘  └──┘  └──┘└────────────────┘└──┘└──────────┘└┘  └──────┘   
typ  ─────────┘  └─┘ └─┘  └──┘  └──┘└────────────────┘└──┘└──────────┘└┘└┘└──────┘└─┘
doc  ─────────┘  └─┘ └─┘  └──┘  └──┘                  └──┘            └┘  └──────┘   
txt  ─────────┘  └─┘ └─┘  └──┘  └──┘                  └──┘            └┘  └──────┘   
par  ─────────┘  └─┘ └─┘  └──┘  └──┘                  └──┘            └┘  └──────┘   
pid  ─────────┘  └─┘ └─┘  └──┘  └───┘                  └──┘            └┘  └───────┘   
st   ──────────────────────────┘└─────────────────────┘└──────────────┘└──┘└───────────
296          | -[1+ k], hk := by rw [int.nat_abs_of_neg_succ_of_nat,
id             └──┘                 └────────────────────────────┘
src  ─────────┘└──┘ └┘  └──┘  └──┘└────────────────────────────┘└─
typ  ─────────┘└──┘ └┘  └──┘  └──┘└────────────────────────────┘└─
doc  ─────────┘      └┘  └──┘  └──┘                              └─
txt  ─────────┘      └┘  └──┘  └──┘                              └─
par  ─────────┘      └┘  └──┘  └──┘                              └─
pid  ─────────┘      └┘  └──┘  └───┘                              └─
st   ───────┘└─────────────────┘└─────────────────────────────────┘└─
297            ← is_subgroup.inv_mem_iff H]; simp * at *
id               └─────────────────────┘ 
src  ───────────┘└─────────────────────┘ └┘└───────────
typ  ───────────┘└─────────────────────┘└┘└───────────
doc  ───────────┘                        └┘└───────────
txt  ───────────┘                        └┘└───────────
par  ───────────┘                        └┘└───────────
pid  ───────────┘                        └──────────────
st   ────────────────────────────────────┘└─────────────
298          end⟩,
src  ───────┘└─────
typ  ───────┘└─────
doc  ───────┘└─────
txt  ───────┘└─────
par  ───────┘└─────
pid  ──────────────
st   ───────┘└─────
299    ⟨⟨⟨g ^ nat.find hex, (nat.find_spec hex).2⟩,
id                           └───────────┘
src  ─┘                └┘ └───────────┘   └─────
typ  ─┘                └┘ └───────────┘   └─────
doc  ─┘                └┘                 └─────
txt  ─┘                └┘                 └─────
par  ─┘                └┘                 └─────
pid  ─┘                └┘                 └─────
st   ───────────────────────────────────────────────
300      λ ⟨x, hx⟩, let ⟨k, hk⟩ := hg x in
id          
src  ───┘ └┘ └┘  └─┘     └┘  └───┘   └───
typ  ───┘ └┘└┘  └─┘     └┘  └───┘   └───
doc  ───┘ └┘ └┘  └─┘     └┘  └───┘   └───
txt  ───┘ └┘ └┘  └─┘     └┘  └───┘   └───
par  ───┘ └┘ └┘  └─┘     └┘  └───┘   └───
pid  ───┘ └┘ └┘  └─┘     └┘  └───┘   └───
st   ──────────────────────────────────────
301        have hk₁ : g ^ ((nat.find hex : ℤ) * (k / nat.find hex)) ∈ gpowers (g ^ nat.find hex),
id                                                                  └─────┘
src  ─────┘    └─────┘               └─┘ └┘             └─┘ └─────┘              └──
typ  ─────┘    └─────┘               └─┘ └┘             └─┘ └─────┘              └──
doc  ─────┘    └─────┘               └─┘ └┘               └─┘                      └──
txt  ─────┘    └─────┘               └─┘ └┘               └─┘                      └──
par  ─────┘    └─────┘               └─┘ └┘               └─┘                      └──
pid  ─────┘    └─────┘               └─┘ └┘               └─┘                      └──
st   ─────────────────────────────────────────────────────────────────────────────────────────────
302          from ⟨k / nat.find hex, eq.symm $ gpow_mul _ _ _⟩,
id                     └──────┘      └─────┘   └──────┘
src  ────────────┘   └──────┘   └┘└─────┘ └──────┘└────────
typ  ────────────┘   └──────┘   └┘└─────┘ └──────┘└────────
doc  ────────────┘              └┘                └────────
txt  ────────────┘              └┘                └────────
par  ────────────┘              └┘                └────────
pid  ────────────┘              └┘                └────────
st   ───────────────────────────────────────────────────────────
303        have hk₂ : g ^ ((nat.find hex : ℤ) * (k / nat.find hex)) ∈ H,
src  ─────┘    └─────┘               └─┘ └┘               └─┘  └─
typ  ─────┘    └─────┘               └─┘ └┘               └─┘  └─
doc  ─────┘    └─────┘               └─┘ └┘               └─┘  └─
txt  ─────┘    └─────┘               └─┘ └┘               └─┘  └─
par  ─────┘    └─────┘               └─┘ └┘               └─┘  └─
pid  ─────┘    └─────┘               └─┘ └┘               └─┘  └─
st   ────────────────────────────────────────────────────────────────────
304          by rw gpow_mul; exact is_subgroup.gpow_mem (nat.find_spec hex).2,
id                 └──────┘        └──────────────────┘  └───────────┘ └─┘
src  ──────────┘└─┘└──────┘└──────┘└──────────────────┘ └───────────┘   └────
typ  ──────────┘└─┘└──────┘└──────┘└──────────────────┘ └───────────┘└─┘└────
doc  ──────────┘└─┘        └──────┘                                     └────
txt  ──────────┘└─┘        └──────┘                                     └────
par  ──────────┘└─┘        └──────┘                                     └────
pid  ─────────────┘        └──────┘                                     └────
st   ─────────┘└────────────────────────────────────────────────────────────┘└─
305        have hk₃ : g ^ (k % nat.find hex) ∈ H,
id                           
src  ─────┘    └─────┘               └┘  └─
typ  ─────┘    └─────┘               └┘  └─
doc  ─────┘    └─────┘                └┘  └─
txt  ─────┘    └─────┘                └┘  └─
par  ─────┘    └─────┘                └┘  └─
pid  ─────┘    └─────┘                └┘  └─
st   ─────────────────────────────────────────────
306          from (is_subgroup.mul_mem_cancel_left H hk₂).1 $
id                 └─────────────────────────────┘
src  ────────────┘ └─────────────────────────────┘    └──┘ 
typ  ────────────┘ └─────────────────────────────┘    └──┘ 
doc  ────────────┘                                    └──┘ 
txt  ────────────┘                                    └──┘ 
par  ────────────┘                                    └──┘ 
pid  ────────────┘                                    └──┘ 
st   ─────────────────────────────────────────────────────────
307            by rw [← gpow_add, int.mod_add_div, hk]; exact hx,
id                      └──────┘  └─────────────┘  └┘         └┘
src  ─────────┘  └────┘└──────┘└┘└─────────────┘└┘  └──────┘  └─
typ  ─────────┘  └────┘└──────┘└┘└─────────────┘└┘└┘└──────┘└┘└─
doc  ─────────┘  └────┘        └┘               └┘  └──────┘  └─
txt  ─────────┘  └────┘        └┘               └┘  └──────┘  └─
par  ─────────┘  └────┘        └┘               └┘  └──────┘  └─
pid  ─────────┘  └─────┘        └┘               └┘  └───────┘  └─
st   ───────────┘└─────────────┘└───────────────┘└──┘└────────┘└─
308        have hk₄ : k % nat.find hex = (k % nat.find hex).nat_abs,
id                                     
src  ─────┘    └─────┘                           └──────────
typ  ─────┘    └─────┘                           └──────────
doc  ─────┘    └─────┘                            └──────────
txt  ─────┘    └─────┘                            └──────────
par  ─────┘    └─────┘                            └──────────
pid  ─────┘    └─────┘                            └──────────
st   ────────────────────────────────────────────────────────────────
309          by rw int.nat_abs_of_nonneg (int.mod_nonneg _
id                 └───────────────────┘  └────────────┘
src  ──────────┘└─┘└───────────────────┘ └────────────┘└──
typ  ──────────┘└─┘└───────────────────┘ └────────────┘└──
doc  ──────────┘└─┘                                    └──
txt  ──────────┘└─┘                                    └──
par  ──────────┘└─┘                                    └──
pid  ─────────────┘                                    └──
st   ─────────┘└───────────────────────────────────────────
310            (int.coe_nat_ne_zero_iff_pos.2 (nat.find_spec hex).1)),
id              └─────────────────────────┘    └───────────┘ └─┘
src  ─────────┘ └─────────────────────────┘└─┘ └───────────┘   └───┘└─
typ  ─────────┘ └─────────────────────────┘└─┘ └───────────┘└─┘└───┘└─
doc  ─────────┘                            └─┘                 └───┘└─
txt  ─────────┘                            └─┘                 └───┘└─
par  ─────────┘                            └─┘                 └───┘└─
pid  ─────────┘                            └─┘                 └──────
st   ───────────────────────────────────────────────────────────────┘└─
311        have hk₅ : g ^ (k % nat.find hex ).nat_abs ∈ H,
id                                      └─┘
src  ─────┘    └─────┘                └─────────┘  └─
typ  ─────┘    └─────┘             └─┘└─────────┘  └─
doc  ─────┘    └─────┘                └─────────┘  └─
txt  ─────┘    └─────┘                └─────────┘  └─
par  ─────┘    └─────┘                └─────────┘  └─
pid  ─────┘    └─────┘                └─────────┘  └─
st   ──────────────────────────────────────────────────────
312          by rwa [← gpow_coe_nat, ← hk₄],
id                     └──────────┘    └─┘
src  ──────────┘└─────┘└──────────┘└──┘   └─
typ  ──────────┘└─────┘└──────────┘└──┘└─┘└─
doc  ──────────┘└─────┘            └──┘   └─
txt  ──────────┘└─────┘            └──┘   └─
par  ──────────┘└─────┘            └──┘   └─
pid  ─────────────────┘            └──┘   └──
st   ─────────┘└──────────────────┘└─────┘└─
313        have hk₆ : (k % (nat.find hex : ℤ)).nat_abs = 0,
id                                   └─┘
src  ─────┘    └─────┘               └─┘ └─────────┘ └───
typ  ─────┘    └─────┘            └─┘└─┘ └─────────┘ └───
doc  ─────┘    └─────┘               └─┘ └─────────┘ └───
txt  ─────┘    └─────┘               └─┘ └─────────┘ └───
par  ─────┘    └─────┘               └─┘ └─────────┘ └───
pid  ─────┘    └─────┘               └─┘ └─────────┘ └───
st   ───────────────────────────────────────────────────────
314          from by_contradiction (λ h,
id                └──────────────┘
src  ────────────┘└──────────────┘  └───
typ  ────────────┘└──────────────┘  └───
doc  ────────────┘                  └───
txt  ────────────┘                  └───
par  ────────────┘                  └───
pid  ────────────┘                  └───
st   ────────────────────────────────────
315            nat.find_min hex (int.coe_nat_lt.1 $ by rw [← hk₄];
id             └──────────┘      └────────────┘              └─┘
src  ─────────┘└──────────┘    └────────────┘└─┘   └────┘   └─
typ  ─────────┘└──────────┘    └────────────┘└─┘   └────┘└─┘└─
doc  ─────────┘                              └─┘   └────┘   └─
txt  ─────────┘                              └─┘   └────┘   └─
par  ─────────┘                              └─┘   └────┘   └─
pid  ─────────┘                              └─┘   └─────┘   └──
st   ────────────────────────────────────────────────┘└────────┘└─
316              exact int.mod_lt_of_pos _ (int.coe_nat_pos.2 (nat.find_spec hex).1))
id                     └───────────────┘    └─────────────┘    └───────────┘ └─┘
src  ─────────────────┘└───────────────┘└─┘ └─────────────┘└─┘ └───────────┘   └─────
typ  ─────────────────┘└───────────────┘└─┘ └─────────────┘└─┘ └───────────┘└─┘└─────
doc  ─────────────────┘                 └─┘                └─┘                 └─────
txt  ─────────────────┘                 └─┘                └─┘                 └─────
par  ─────────────────┘                 └─┘                └─┘                 └─────
pid  ─────────────────┘                 └─┘                └─┘                 └─────
st   ──────────────────────────────────────────────────────────────────────────────┘└─
317            ⟨nat.pos_of_ne_zero h, hk₅⟩),
src  ─────────┘                    └┘   └───
typ  ─────────┘                    └┘   └───
doc  ─────────┘                    └┘   └───
txt  ─────────┘                    └┘   └───
par  ─────────┘                    └┘   └───
pid  ─────────┘                    └┘   └───
st   ────────────────────────────────────────
318        ⟨k / (nat.find hex : ℤ), subtype.coe_ext.2 begin
id                        └─┘       └─────────────┘
src  ─────┘               └─┘ └─┘└─────────────┘└─┘     
typ  ─────┘            └─┘└─┘ └─┘└─────────────┘└─┘     
doc  ─────┘               └─┘ └─┘               └─┘     
txt  ─────┘               └─┘ └─┘               └─┘     
par  ─────┘               └─┘ └─┘               └─┘     
pid  ─────┘               └─┘ └─┘               └─┘     
st   ────────────────────────────────────────────────┘└─────
319          suffices : g ^ ((nat.find hex : ℤ) * (k / nat.find hex)) = x,
id                                                   └──────┘ └─┘     
src  ───────┘└─────────┘               └─┘ └┘    └──────┘   └─┘  └─
typ  ───────┘└─────────┘              └─┘ └┘   └──────┘└─┘└─┘ └─
doc  ───────┘└─────────┘               └─┘ └┘               └─┘  └─
txt  ───────┘└─────────┘               └─┘ └┘               └─┘  └─
par  ───────┘└─────────┘               └─┘ └┘               └─┘  └─
pid  ──────────────────┘               └─┘ └┘               └─┘  └─
st   ───────────────────────────────────────────────────────────────────┘└─
320          { simpa [gpow_mul] },
id                    └──────┘
src  ─────────┘└─────┘└──────┘└┘└──
typ  ─────────┘└─────┘└──────┘└┘└──
doc  ─────────┘└─────┘        └┘└──
txt  ─────────┘└─────┘        └┘└──
par  ─────────┘└─────┘        └┘└──
pid  ────────────────┘        └────
st   ────────┘└────────────────┘└─
321          rw [int.mul_div_cancel' (int.dvd_of_mod_eq_zero (int.eq_zero_of_nat_abs_eq_zero hk₆)), hk]
id               └─────────────────┘  └────────────────────┘  └────────────────────────────┘ └─┘    └┘
src  ───────┘└──┘└─────────────────┘ └────────────────────┘ └────────────────────────────┘   └──┘  └─
typ  ───────┘└──┘└─────────────────┘ └────────────────────┘ └────────────────────────────┘└─┘└──┘└┘└─
doc  ───────┘└──┘                                                                            └──┘  └─
txt  ───────┘└──┘                                                                            └──┘  └─
par  ───────┘└──┘                                                                            └──┘  └─
pid  ───────────┘                                                                            └──┘  └─
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└──┘
322        end⟩⟩⟩
src  ─────┘└──────
typ  ─────┘└──────
doc  ─────┘└──────
txt  ─────┘└──────
par  ─────┘└──────
pid  ─────────────
st   ─────┘└─┘└───
323  else
src  ─────
typ  ─────
doc  ─────
txt  ─────
par  ─────
pid  ─────
st   ─────
324    have H = is_subgroup.trivial α,
id     └──┘     └─────────────────┘
src  ─┘└──┘└─┘ └─────────────────┘ └─
typ  ─┘└──┘└─┘ └─────────────────┘ └─
doc  ─┘    └─┘ └─────────────────┘ └─
txt  ─┘    └─┘                     └─
par  ─┘    └─┘                     └─
pid  ─┘    └─┘                     └─
st   ──────────────────────────────────
325      from set.ext $ λ x, ⟨λ h, by simp at *; tauto,
id            └─────┘
src  ────────┘└─────┘  └──┘  └──┘  └───────┘└┘└───┘└─
typ  ────────┘└─────┘  └──┘  └──┘  └───────┘└┘└───┘└─
doc  ────────┘         └──┘  └──┘  └───────┘└┘└───┘└─
txt  ────────┘         └──┘  └──┘  └───────┘└┘└───┘└─
par  ────────┘         └──┘  └──┘  └───────┘└┘└───┘└─
pid  ────────┘         └──┘  └──┘  └──────────────────
st   ───────────────────────────────┘└───────────────┘└─
326        λ h, by rw [is_subgroup.mem_trivial.1 h]; exact is_submonoid.one_mem _⟩,
id                     └─────────────────────┘            └──────────────────┘
src  ─────┘ └──┘  └──┘└─────────────────────┘└─┘ └──────┘└──────────────────┘└────
typ  ─────┘ └──┘  └──┘└─────────────────────┘└─┘└──────┘└──────────────────┘└────
doc  ─────┘ └──┘  └──┘                       └─┘ └──────┘                    └────
txt  ─────┘ └──┘  └──┘                       └─┘ └──────┘                    └────
par  ─────┘ └──┘  └──┘                       └─┘ └──────┘                    └────
pid  ─────┘ └──┘  └───┘                       └─┘ └───────┘                    └────
st   ────────────┘└──────────────────────────────┘└────────────────────────────┘└──
327    by clear _let_match; subst this; apply_instance
id                                └──┘
src  ─┘  └──────────────┘└┘└────┘    └┘└──────────────
typ  ─┘  └──────────────┘└──────┘└──┘└┘└──────────────
doc  ─┘  └──────────────┘└┘└────┘    └┘└──────────────
txt  ─┘  └──────────────┘└┘└────┘    └┘└──────────────
par  ─┘  └──────────────┘└──────┘    └┘└──────────────
pid  ─┘  └───────────────────────┘    └────────────────
st   ───┘└─────────────────────────────────────────────
328  
src  
typ  
doc  
txt  
par  
pid  
st   
329  open finset nat
330  
331  lemma is_cyclic.card_pow_eq_one_le [group α] [fintype α] [decidable_eq α] [is_cyclic α] {n : ℕ}
id                                       └───┘    └─────┘    └──────────┘    └───────┘        
src                                      └───┘     └─────┘     └──────────┘     └───────┘         
typ                                      └───┘    └─────┘    └──────────┘    └───────┘        
doc                                                └─────┘
332    (hn0 : 0 < n) : (univ.filter (λ a : α, a ^ n = 1)).card ≤ n :=
id                    └──┘└─────┘                 └──┘   
src                    └──┘└─────┘                    └──┘  
typ                   └──┘└─────┘                 └──┘   
doc                     └──┘└─────┘                      └──┘
333  let ⟨g, hg⟩ := is_cyclic.exists_generator α in
id   └─┘    └┘     └────────────────────────┘ 
src                 └────────────────────────┘
typ  └─┘    └┘     └────────────────────────┘ 
334  calc (univ.filter (λ a : α, a ^ n = 1)).card ≤ (gpowers (g ^ (fintype.card α / (gcd n (fintype.card α))))).to_finset.card :
id         └──┘└─────┘                 └──┘     └─────┘      └──────────┘    └─┘   └──────────┘      └───────┘ └──┘
src        └──┘└─────┘                    └──┘     └─────┘      └──────────┘     └─┘    └──────────┘       └───────┘ └──┘
typ        └──┘└─────┘                 └──┘     └─────┘      └──────────┘    └─┘   └──────────┘      └───────┘ └──┘
doc        └──┘└─────┘                      └──┘                   └──────────┘             └──────────┘       └───────┘ └──┘
335    card_le_of_subset (λ x hx, let ⟨m, hm⟩ := show x ∈ powers g, from (powers_eq_gpowers g).symm ▸ hg x in
id     └───────────────┘     └┘  └─┘                  └────┘          └───────────────┘   └──┘      
src    └───────────────┘                                 └────┘          └───────────────┘   └──┘  
typ    └───────────────┘     └┘  └─┘                  └────┘          └───────────────┘   └──┘      
doc                                                       └────┘
336      set.mem_to_finset.2 ⟨(m / (fintype.card α / (gcd n (fintype.card α))) : ℕ),
id       └───────────────┘        └──────────┘    └─┘   └──────────┘       
src      └───────────────┘        └──────────┘     └─┘    └──────────┘        
typ      └───────────────┘        └──────────┘    └─┘   └──────────┘       
doc                                 └──────────┘             └──────────┘
337        have hgmn : g ^ (m * gcd n (fintype.card α)) = 1,
id                            └─┘   └──────────┘    
src                           └─┘    └──────────┘     
typ                           └─┘   └──────────┘    
doc                                    └──────────┘
338          by rw [pow_mul, hm, ← pow_gcd_card_eq_one_iff]; exact (mem_filter.1 hx).2,
id                  └─────┘  └┘    └─────────────────────┘          └────────┘   └┘
src             └──┘└─────┘└┘  └──┘└─────────────────────┘  └────┘ └────────┘└─┘  └─┘
typ             └──┘└─────┘└┘└┘└──┘└─────────────────────┘  └────┘ └────────┘└─┘└┘└─┘
doc             └──┘       └┘  └──┘                         └────┘           └─┘  └─┘
txt             └──┘       └┘  └──┘                         └────┘           └─┘  └─┘
par             └──┘       └┘  └──┘                         └────┘           └─┘  └─┘
pid               └┘       └┘  └──┘                                         └─┘  └┘
st             └──────────┘└──┘└─────────────────────────┘└─────────────────────────┘
339        begin
st         └─────
340          rw [gpow_coe_nat, ← pow_mul, nat.mul_div_cancel_left', hm],
id               └──────────┘    └─────┘  └──────────────────────┘  └┘
src          └──┘└──────────┘└──┘└─────┘└┘└──────────────────────┘└┘  
typ          └──┘└──────────┘└──┘└─────┘└┘└──────────────────────┘└┘└┘
doc          └──┘            └──┘       └┘                        └┘  
txt          └──┘            └──┘       └┘                        └┘  
par          └──┘            └──┘       └┘                        └┘  
pid            └┘            └──┘       └┘                        └┘  
st   ───────────────────────┘└─────────┘└────────────────────────┘└──┘└──
341          refine dvd_of_mul_dvd_mul_right (gcd_pos_of_pos_left (fintype.card α) hn0) _,
id                  └──────────────────────┘  └─────────────────┘  └──────────┘   └─┘
src          └─────┘└──────────────────────┘ └─────────────────┘ └──────────┘ └┘   └─┘
typ          └─────┘└──────────────────────┘ └─────────────────┘ └──────────┘└┘└─┘└─┘
doc          └─────┘                                             └──────────┘ └┘   └─┘
txt          └─────┘                                                          └┘   └─┘
par          └─────┘                                                          └┘   └─┘
pid                                                                          └┘   └─┘
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
342          conv {to_lhs, rw [nat.div_mul_cancel (gcd_dvd_right _ _), ← order_of_eq_card_of_forall_mem_gpowers hg]},
id                             └────────────────┘  └───────────┘         └────────────────────────────────────┘ └┘
src          └────┘└────┘└┘└──┘└────────────────┘ └───────────┘└───────┘└────────────────────────────────────┘  
typ          └────┘└────┘└┘└──┘└────────────────┘ └───────────┘└───────┘└────────────────────────────────────┘└┘
txt          └────┘└────┘└┘└──┘                                └───────┘                                        
par          └────┘└────┘└┘└──┘                                └───────┘                                        
pid              └───────────┘                                └───────┘                                        └┘
st   ─────────────┘└────┘└──────────────────────────────────────────┘└───────────────────────────────────────────┘ └┘
343          exact order_of_dvd_of_pow_eq_one hgmn
id                 └────────────────────────┘ └──┘
src          └────┘└────────────────────────┘    
typ          └────┘└────────────────────────┘└──┘
doc          └────┘                              
txt          └────┘                              
par          └────┘                              
pid                                             
st   ──────────────────────────────────────────────
344        end⟩)
src  ─────┘
typ  ─────┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘└─┘
345  ... ≤ n :
id         
typ        
346    let ⟨m, hm⟩ := gcd_dvd_right n (fintype.card α) in
id     └─┘           └───────────┘   └──────────┘ 
src                   └───────────┘    └──────────┘
typ    └─┘           └───────────┘   └──────────┘ 
doc                                    └──────────┘
347    have hm0 : 0 < m, from nat.pos_of_ne_zero
id                           └────────────────┘
src                          └────────────────┘
typ                          └────────────────┘
348      (λ hm0, (by rw [hm0, mul_zero, fintype.card_eq_zero_iff] at hm; exact hm 1)),
id          └─┘          └─┘  └──────┘  └──────────────────────┘               └┘
src                  └──┘   └┘└──────┘└┘└──────────────────────┘└─────┘  └────┘  └┘
typ         └─┘      └──┘└─┘└┘└──────┘└┘└──────────────────────┘└─────┘  └────┘└┘└┘
doc                  └──┘   └┘        └┘                        └─────┘  └────┘  └┘
txt                  └──┘   └┘        └┘                        └─────┘  └────┘  └┘
par                  └──┘   └┘        └┘                        └─────┘  └────┘  └┘
pid                    └┘   └┘        └┘                        └────┘         
st                  └──────┘└────────┘└────────────────────────┘└────────────────┘
349    begin
st     └─────
350      rw [← fintype.card_of_finset' _ (λ _, set.mem_to_finset), ← order_eq_card_gpowers,
id             └─────────────────────┘         └───────────────┘     └───────────────────┘
src      └────┘└─────────────────────┘└─┘  └──┘└───────────────┘└───┘└───────────────────┘└─
typ      └────┘└─────────────────────┘└─┘  └──┘└───────────────┘└───┘└───────────────────┘└─
doc      └────┘                       └─┘  └──┘                 └───┘                     └─
txt      └────┘                       └─┘  └──┘                 └───┘                     └─
par      └────┘                       └─┘  └──┘                 └───┘                     └─
pid        └──┘                       └─┘  └──┘                 └───┘                     └─
st   ───────────────────────────────────────────────────────────┘└───────────────────────┘└─
351        order_of_pow, order_of_eq_card_of_forall_mem_gpowers hg],
id         └──────────┘  └────────────────────────────────────┘ └┘
src  ─────┘└──────────┘└┘└────────────────────────────────────┘  
typ  ─────┘└──────────┘└┘└────────────────────────────────────┘└┘
doc  ─────┘            └┘                                        
txt  ─────┘            └┘                                        
par  ─────┘            └┘                                        
pid  ─────┘            └┘                                        
st   ─────────────────┘└─────────────────────────────────────────┘└──
352      rw [hm] {occs := occurrences.pos [2,3]},
id           └┘           └─────────────┘   
src      └──┘  └┘ └──────┘└─────────────┘
typ      └──┘└┘└┘ └──────┘└─────────────┘
doc      └──┘  └┘ └──────┘                  
txt      └──┘  └┘ └──────┘                  
par      └──┘  └┘ └──────┘                  
pid        └┘   └──────┘                  
st   ─────────┘└──────────────────────────────┘└─
353      rw [nat.mul_div_cancel_left _  (gcd_pos_of_pos_left _ hn0), gcd_mul_left_left,
id           └─────────────────────┘     └─────────────────┘   └─┘   └───────────────┘
src      └──┘└─────────────────────┘└──┘ └─────────────────┘└─┘   └─┘└───────────────┘└─
typ      └──┘└─────────────────────┘└──┘ └─────────────────┘└─┘└─┘└─┘└───────────────┘└─
doc      └──┘                       └──┘                    └─┘   └─┘                 └─
txt      └──┘                       └──┘                    └─┘   └─┘                 └─
par      └──┘                       └──┘                    └─┘   └─┘                 └─
pid        └┘                       └──┘                    └─┘   └─┘                 └─
st   ─────────────────────────────────────────────────────────────┘└─────────────────┘└─
354        hm, nat.mul_div_cancel _ hm0],
id         └┘  └────────────────┘   └─┘
src  ─────┘  └┘└────────────────┘└─┘   
typ  ─────┘└┘└┘└────────────────┘└─┘└─┘
doc  ─────┘  └┘                  └─┘   
txt  ─────┘  └┘                  └─┘   
par  ─────┘  └┘                  └─┘   
pid  ─────┘  └┘                  └─┘   
st   ───────┘└────────────────────────┘└──
355      exact le_of_dvd hn0 (gcd_dvd_left _ _)
id             └───────┘ └─┘  └──────────┘
src      └────┘└───────┘    └──────────┘└─────
typ      └────┘└───────┘└─┘ └──────────┘└─────
doc      └────┘                         └─────
txt      └────┘                         └─────
par      └────┘                         └─────
pid                                    └───┘
st   ───────────────────────────────────────────
356    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
357  
358  section totient
359  
360  variables [group α] [fintype α] [decidable_eq α] (hn : ∀ n : ℕ, 0 < n → (univ.filter (λ a : α, a ^ n = 1)).card ≤ n)
id              └───┘     └─────┘     └──────────┘                         └──┘└─────┘                  └──┘   
src             └───┘     └─────┘     └──────────┘                          └──┘└─────┘                    └──┘  
typ             └───┘     └─────┘     └──────────┘                         └──┘└─────┘                  └──┘   
doc                       └─────┘                                             └──┘└─────┘                      └──┘
361  include hn
362  
363  lemma card_pow_eq_one_eq_order_of_aux (a : α) :
id                                              
typ                                             
364    (finset.univ.filter (λ b : α, b ^ order_of a = 1)).card = order_of a :=
id      └─────────┘└─────┘            └──────┘      └──┘   └──────┘ 
src     └─────────┘└─────┘              └──────┘       └──┘   └──────┘
typ     └─────────┘└─────┘            └──────┘      └──┘   └──────┘ 
doc     └─────────┘└─────┘               └──────┘        └──┘    └──────┘
365  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
366    (hn _ (order_of_pos _))
id      └┘    └──────────┘
src           └──────────┘
typ     └┘    └──────────┘
367    (calc order_of a = @fintype.card (gpowers a) (id _) : order_eq_card_gpowers
id           └──────┘     └──────────┘  └─────┘    └┘      └───────────────────┘
src          └──────┘      └──────────┘  └─────┘     └┘      └───────────────────┘
typ          └──────┘     └──────────┘  └─────┘    └┘      └───────────────────┘
doc          └──────┘      └──────────┘
368      ... ≤ @fintype.card (↑(univ.filter (λ b : α, b ^ order_of a = 1)) : set α)
id              └──────────┘   └──┘└─────┘            └──────┘         └─┘ 
src             └──────────┘   └──┘└─────┘              └──────┘          └─┘
typ             └──────────┘   └──┘└─────┘            └──────┘         └─┘ 
doc             └──────────┘    └──┘└─────┘               └──────┘
369      (fintype.of_finset _ (λ _, iff.rfl)) :
id        └───────────────┘        └─────┘
src       └───────────────┘         └─────┘
typ       └───────────────┘        └─────┘
doc       └───────────────┘
370        @fintype.card_le_of_injective (gpowers a) (↑(univ.filter (λ b : α, b ^ order_of a = 1)) : set α)
id          └──────────────────────────┘  └─────┘     └──┘└─────┘            └──────┘         └─┘ 
src         └──────────────────────────┘  └─────┘      └──┘└─────┘              └──────┘          └─┘
typ         └──────────────────────────┘  └─────┘     └──┘└─────┘            └──────┘         └─┘ 
doc                                                     └──┘└─────┘               └──────┘
371          (id _) (id _) (λ b, ⟨b.1, mem_filter.2 ⟨mem_univ _,
id            └┘     └┘             └────────┘   └──────┘
src           └┘     └┘               └────────┘   └──────┘
typ           └┘     └┘             └────────┘   └──────┘
372            let ⟨i, hi⟩ := b.2 in
id             └─┘            
src                            
typ            └─┘            
373            by rw [← hi, ← gpow_coe_nat, ← gpow_mul, mul_comm, gpow_mul, gpow_coe_nat,
id                      └┘    └──────────┘    └──────┘  └──────┘  └──────┘  └──────────┘
src               └────┘  └──┘└──────────┘└──┘└──────┘└┘└──────┘└┘└──────┘└┘└──────────┘└─
typ               └────┘└┘└──┘└──────────┘└──┘└──────┘└┘└──────┘└┘└──────┘└┘└──────────┘└─
doc               └────┘  └──┘            └──┘        └┘        └┘        └┘            └─
txt               └────┘  └──┘            └──┘        └┘        └┘        └┘            └─
par               └────┘  └──┘            └──┘        └┘        └┘        └┘            └─
pid                 └──┘  └──┘            └──┘        └┘        └┘        └┘            └─
st               └───────┘└──────────────┘└──────────┘└────────┘└────────┘└────────────┘└─
374              pow_order_of_eq_one, one_gpow]⟩⟩) (λ _ _ h, subtype.eq (subtype.mk.inj h))
id               └─────────────────┘  └──────┘            └────────┘  └────────────┘ 
src  ───────────┘└─────────────────┘└┘└──────┘              └────────┘  └────────────┘
typ  ───────────┘└─────────────────┘└┘└──────┘           └────────┘  └────────────┘ 
doc  ───────────┘                   └┘        
txt  ───────────┘                   └┘        
par  ───────────┘                   └┘        
pid  ───────────┘                   └┘        
st   ──────────────────────────────┘└────────┘
375      ... = (univ.filter (λ b : α, b ^ order_of a = 1)).card : fintype.card_of_finset _ _)
id              └──┘└─────┘            └──────┘      └──┘    └────────────────────┘
src             └──┘└─────┘              └──────┘       └──┘    └────────────────────┘
typ             └──┘└─────┘            └──────┘      └──┘    └────────────────────┘
doc             └──┘└─────┘               └──────┘        └──┘
376  
377  open_locale nat -- use φ for nat.totient
378  
379  private lemma card_order_of_eq_totient_aux₁ :
380    ∀ {d : ℕ}, d ∣ fintype.card α → 0 < (univ.filter (λ a : α, order_of a = d)).card →
id                └──────────┘        └──┘└─────┘          └──────┘     └──┘
src                 └──────────┘         └──┘└─────┘           └──────┘       └──┘
typ               └──────────┘        └──┘└─────┘          └──────┘     └──┘
doc                   └──────────┘          └──┘└─────┘           └──────┘        └──┘
381    (univ.filter (λ a : α, order_of a = d)).card = φ d
id      └──┘└─────┘          └──────┘     └──┘    
src     └──┘└─────┘           └──────┘       └──┘   
typ     └──┘└─────┘          └──────┘     └──┘    
doc     └──┘└─────┘           └──────┘        └──┘
382  | 0     := λ hd hd0,
id                └┘ └─┘
typ               └┘ └─┘
383  let ⟨a, ha⟩ := card_pos.1 hd0 in absurd (mem_filter.1 ha).2 $ ne_of_gt $ order_of_pos a
id   └─┘    └┘     └──────┘  └─┘    └────┘  └────────┘         └──────┘   └──────────┘
src                 └──────┘         └────┘  └────────┘         └──────┘   └──────────┘
typ  └─┘    └┘     └──────┘  └─┘    └────┘  └────────┘         └──────┘   └──────────┘
384  | (d+1) := λ hd hd0,
id              └┘ └─┘
src      
typ             └┘ └─┘
385  let ⟨a, ha⟩ := card_pos.1 hd0 in
id   └─┘    └┘     └──────┘  └─┘
src                 └──────┘
typ  └─┘    └┘     └──────┘  └─┘
386  have ha : order_of a = d.succ, from (mem_filter.1 ha).2,
id             └──────┘     └───┘        └────────┘     
src            └──────┘     └───┘        └────────┘     
typ            └──────┘     └───┘        └────────┘     
doc            └──────┘
387  have h : ((range d.succ).filter (∣ d.succ)).sum
id              └───┘  └───┘ └────┘     └───┘  └─┘
src             └───┘  └───┘ └────┘     └───┘  └─┘
typ             └───┘  └───┘ └────┘     └───┘  └─┘
doc             └───┘        └────┘
388      (λ m, (univ.filter (λ a : α, order_of a = m)).card) =
id             └──┘└─────┘          └──────┘     └──┘   
src             └──┘└─────┘           └──────┘       └──┘   
typ            └──┘└─────┘          └──────┘     └──┘   
doc             └──┘└─────┘           └──────┘        └──┘
389      ((range d.succ).filter (∣ d.succ)).sum φ, from
id         └───┘  └───┘ └────┘     └───┘  └─┘  
src        └───┘  └───┘ └────┘     └───┘  └─┘  
typ        └───┘  └───┘ └────┘     └───┘  └─┘  
doc        └───┘        └────┘
390    finset.sum_congr rfl
id     └──────────────┘ └─┘
src    └──────────────┘ └─┘
typ    └──────────────┘ └─┘
391      (λ m hm, have hmd : m < d.succ, from mem_range.1 (mem_filter.1 hm).1,
id           └┘                └───┘       └───────┘   └────────┘  └┘ 
src                              └───┘       └───────┘   └────────┘     
typ          └┘                └───┘       └───────┘   └────────┘  └┘ 
392        have hm : m ∣ d.succ, from (mem_filter.1 hm).2,
id                      └───┘        └────────┘  └┘ 
src                      └───┘        └────────┘     
typ                     └───┘        └────────┘  └┘ 
393        card_order_of_eq_totient_aux₁ (dvd.trans hm hd) (finset.card_pos.2
id         └───────────────────────────┘  └───────┘ └┘ └┘   └─────────────┘
src                                       └───────┘         └─────────────┘
typ        └───────────────────────────┘  └───────┘ └┘ └┘   └─────────────┘
394          ⟨a ^ (d.succ / m), mem_filter.2 ⟨mem_univ _,
id                 └───┘     └────────┘   └──────┘
src                └───┘      └────────┘   └──────┘
typ                └───┘     └────────┘   └──────┘
395            by rw [order_of_pow, ha, gcd_eq_right (div_dvd_of_dvd hm),
id                    └──────────┘  └┘  └──────────┘  └────────────┘ └┘
src               └──┘└──────────┘└┘  └┘└──────────┘ └────────────┘  └──
typ               └──┘└──────────┘└┘└┘└┘└──────────┘ └────────────┘└┘└──
doc               └──┘            └┘  └┘                             └──
txt               └──┘            └┘  └┘                             └──
par               └──┘            └┘  └┘                             └──
pid                 └┘            └┘  └┘                             └──
st               └───────────────┘└──┘└────────────────────────────────┘└─
396              nat.div_div_self hm (succ_pos _)]⟩⟩)),
id               └──────────────┘ └┘  └──────┘
src  ───────────┘└──────────────┘   └──────┘└──┘
typ  ───────────┘└──────────────┘└┘ └──────┘└──┘
doc  ───────────┘                           └──┘
txt  ───────────┘                           └──┘
par  ───────────┘                           └──┘
pid  ───────────┘                           └──┘
st   ───────────────────────────────────────────┘
397  have hinsert : insert d.succ ((range d.succ).filter (∣ d.succ))
id                  └────┘  └───┘   └───┘  └───┘ └────┘     └───┘
src                 └────┘  └───┘   └───┘  └───┘ └────┘     └───┘
typ                 └────┘  └───┘   └───┘  └───┘ └────┘     └───┘
doc                                 └───┘        └────┘
398      = (range d.succ.succ).filter (∣ d.succ),
id         └───┘  └────────┘ └────┘     └───┘
src        └───┘  └────────┘ └────┘     └───┘
typ        └───┘  └────────┘ └────┘     └───┘
doc         └───┘             └────┘
399    from (finset.ext.2 $ λ x, ⟨λ h, (mem_insert.1 h).elim (λ h, by simp [h, range_succ])
id           └────────┘              └────────┘   └──┘                  └────────┘
src          └────────┘                └────────┘    └──┘           └────┘ └┘└────────┘
typ          └────────┘              └────────┘   └──┘          └────┘└┘└────────┘
doc                                                                   └────┘ └┘          
txt                                                                   └────┘ └┘          
par                                                                   └────┘ └┘          
pid                                                                        └┘          
st                                                                   └───────────────────┘
400      (by clear _let_match; simp [range_succ]; tauto), by clear _let_match; simp [range_succ] {contextual := tt}; tauto⟩),
id                                   └────────┘                                      └────────┘                 └┘
src          └──────────────┘  └────┘└────────┘  └───┘      └──────────────┘  └────┘└────────┘└┘ └────────────┘└┘  └───┘
typ          └──────────────┘  └────┘└────────┘  └───┘      └──────────────┘  └────┘└────────┘└┘ └────────────┘└┘  └───┘
doc          └──────────────┘  └────┘            └───┘      └──────────────┘  └────┘          └┘ └────────────┘    └───┘
txt          └──────────────┘  └────┘            └───┘      └──────────────┘  └────┘          └┘ └────────────┘    └───┘
par          └──────────────┘  └────┘            └───┘      └──────────────┘  └────┘          └┘ └────────────┘    └───┘
pid               └─────────┘                                  └─────────┘                 └────────────┘  
st          └─────────────────────────────────────────┘     └────────────────────────────────────────────────────────────┘
401  have hinsert₁ : d.succ ∉ (range d.succ).filter (∣ d.succ),
id                    └───┘   └───┘  └───┘ └────┘     └───┘
src                   └───┘   └───┘  └───┘ └────┘     └───┘
typ                   └───┘   └───┘  └───┘ └────┘     └───┘
doc                            └───┘        └────┘
402    by simp [mem_range, zero_le_one, le_succ],
id              └───────┘  └─────────┘  └─────┘
src       └────┘└───────┘└┘└─────────┘└┘└─────┘
typ       └────┘└───────┘└┘└─────────┘└┘└─────┘
doc       └────┘         └┘           └┘       
txt       └────┘         └┘           └┘       
par       └────┘         └┘           └┘       
pid                    └┘           └┘       
st       └─────────────────────────────────────┘
403  (add_right_inj (((range d.succ).filter (∣ d.succ)).sum
id    └───────────┘    └───┘  └───┘ └────┘     └───┘  └─┘
src   └───────────┘    └───┘  └───┘ └────┘     └───┘  └─┘
typ   └───────────┘    └───┘  └───┘ └────┘     └───┘  └─┘
doc                    └───┘        └────┘
404    (λ m, (univ.filter (λ a : α, order_of a = m)).card))).1
id           └──┘└─────┘          └──────┘     └──┘    
src           └──┘└─────┘           └──────┘       └──┘    
typ          └──┘└─────┘          └──────┘     └──┘    
doc           └──┘└─────┘           └──────┘        └──┘
405    (calc _ = (insert d.succ (filter (∣ d.succ) (range d.succ))).sum
id                └────┘  └───┘  └────┘    └───┘   └───┘  └───┘   └─┘
src               └────┘  └───┘  └────┘    └───┘   └───┘  └───┘   └─┘
typ               └────┘  └───┘  └────┘    └───┘   └───┘  └───┘   └─┘
doc                              └────┘             └───┘
406          (λ m, (univ.filter (λ a : α, order_of a = m)).card) :
id                 └──┘└─────┘          └──────┘     └──┘
src                 └──┘└─────┘           └──────┘       └──┘
typ                └──┘└─────┘          └──────┘     └──┘
doc                 └──┘└─────┘           └──────┘        └──┘
407      eq.symm (finset.sum_insert (by simp [mem_range, zero_le_one, le_succ]))
id       └─────┘  └───────────────┘           └───────┘  └─────────┘  └─────┘
src      └─────┘  └───────────────┘     └────┘└───────┘└┘└─────────┘└┘└─────┘
typ      └─────┘  └───────────────┘     └────┘└───────┘└┘└─────────┘└┘└─────┘
doc                                     └────┘         └┘           └┘       
txt                                     └────┘         └┘           └┘       
par                                     └────┘         └┘           └┘       
pid                                                  └┘           └┘       
st                                     └─────────────────────────────────────┘
408    ... = ((range d.succ.succ).filter (∣ d.succ)).sum (λ m,
id             └───┘  └────────┘ └────┘     └───┘  └─┘     
src            └───┘  └────────┘ └────┘     └───┘  └─┘
typ            └───┘  └────────┘ └────┘     └───┘  └─┘     
doc            └───┘             └────┘
409        (univ.filter (λ a : α, order_of a = m)).card) :
id          └──┘└─────┘          └──────┘     └──┘
src         └──┘└─────┘           └──────┘       └──┘
typ         └──┘└─────┘          └──────┘     └──┘
doc         └──┘└─────┘           └──────┘        └──┘
410      sum_congr hinsert (λ _ _, rfl)
id       └───────┘ └─────┘       └─┘
src      └───────┘                 └─┘
typ      └───────┘ └─────┘       └─┘
411    ... = (univ.filter (λ a : α, a ^ d.succ = 1)).card :
id            └──┘└─────┘             └───┘     └──┘
src           └──┘└─────┘               └───┘     └──┘
typ           └──┘└─────┘             └───┘     └──┘
doc           └──┘└─────┘                           └──┘
412      sum_card_order_of_eq_card_pow_eq_one (succ_pos d)
id       └──────────────────────────────────┘  └──────┘
src      └──────────────────────────────────┘  └──────┘
typ      └──────────────────────────────────┘  └──────┘
413    ... = ((range d.succ.succ).filter (∣ d.succ)).sum φ :
id             └───┘  └────────┘ └────┘     └───┘  └─┘  
src            └───┘  └────────┘ └────┘     └───┘  └─┘  
typ            └───┘  └────────┘ └────┘     └───┘  └─┘  
doc            └───┘             └────┘
414      ha ▸ (card_pow_eq_one_eq_order_of_aux hn a).symm ▸ (sum_totient _).symm
id       └┘   └─────────────────────────────┘ └┘   └──┘    └─────────┘   └──┘
src           └─────────────────────────────┘      └──┘    └─────────┘   └──┘
typ      └┘   └─────────────────────────────┘ └┘   └──┘    └─────────┘   └──┘
415    ... = _ : by rw [h, ← sum_insert hinsert₁];
id                          └────────┘ └──────┘
src                 └──┘ └──┘└────────┘        
typ                 └──┘└──┘└────────┘└──────┘
doc                 └──┘ └──┘                  
txt                 └──┘ └──┘                  
par                 └──┘ └──┘                  
pid                   └┘ └──┘                  
st                 └────┘└─────────────────────┘└─
416        exact finset.sum_congr hinsert.symm (λ _ _, rfl))
id               └──────────────┘ └──────────┘         └─┘
src        └────┘└──────────────┘└──────────┘  └────┘└─┘
typ        └────┘└──────────────┘└──────────┘  └────┘└─┘
doc        └────┘                              └────┘   
txt        └────┘                              └────┘   
par        └────┘                              └────┘   
pid                                           └────┘   
st   ─────────────────────────────────────────────────────┘
417  
418  lemma card_order_of_eq_totient_aux₂ {d : ℕ} (hd : d ∣ fintype.card α) :
id                                                      └──────────┘ 
src                                                      └──────────┘
typ                                                     └──────────┘ 
doc                                                        └──────────┘
419    (univ.filter (λ a : α, order_of a = d)).card = φ d :=
id      └──┘└─────┘          └──────┘     └──┘    
src     └──┘└─────┘           └──────┘       └──┘   
typ     └──┘└─────┘          └──────┘     └──┘    
doc     └──┘└─────┘           └──────┘        └──┘
420  by_contradiction $ λ h,
id   └──────────────┘     
src  └──────────────┘
typ  └──────────────┘     
421  have h0 : (univ.filter (λ a : α , order_of a = d)).card = 0 :=
id              └──┘└─────┘           └──────┘     └──┘  
src             └──┘└─────┘            └──────┘       └──┘  
typ             └──┘└─────┘           └──────┘     └──┘  
doc             └──┘└─────┘            └──────┘        └──┘
422    not_not.1 (mt nat.pos_iff_ne_zero.2 (mt (card_order_of_eq_totient_aux₁ hn hd) h)),
id     └─────┘   └┘ └─────────────────┘   └┘  └───────────────────────────┘ └┘ └┘  
src    └─────┘   └┘ └─────────────────┘   └┘  └───────────────────────────┘
typ    └─────┘   └┘ └─────────────────┘   └┘  └───────────────────────────┘ └┘ └┘  
423  let c := fintype.card α in
id           └──────────┘ 
src           └──────────┘
typ          └──────────┘ 
doc           └──────────┘
424  have hc0 : 0 < c, from fintype.card_pos_iff.2 ⟨1⟩,
id                        └──────────────────┘
src                        └──────────────────┘
typ                       └──────────────────┘
425  lt_irrefl c $
id   └───────┘ 
src  └───────┘
typ  └───────┘ 
426    calc c = (univ.filter (λ a : α, a ^ c = 1)).card :
id              └──┘└─────┘                 └──┘
src              └──┘└─────┘                    └──┘
typ             └──┘└─────┘                 └──┘
doc              └──┘└─────┘                      └──┘
427      congr_arg card $ by simp [finset.ext, c]
id       └───────┘ └──┘            └────────┘  
src      └───────┘ └──┘      └────┘└────────┘└┘ └─
typ      └───────┘ └──┘      └────┘└────────┘└┘└─
doc                └──┘      └────┘          └┘ └─
txt                          └────┘          └┘ └─
par                          └────┘          └┘ └─
pid                                        └┘ 
st                          └─────────────────────
428    ... = ((range c.succ).filter (∣ c)).sum
id             └───┘ └───┘ └────┘      └─┘
src  ─┘        └───┘  └───┘ └────┘       └─┘
typ  ─┘        └───┘ └───┘ └────┘      └─┘
doc  ─┘        └───┘        └────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
429        (λ m, (univ.filter (λ a : α, order_of a = m)).card) :
id               └──┘└─────┘          └──────┘     └──┘
src               └──┘└─────┘           └──────┘       └──┘
typ              └──┘└─────┘          └──────┘     └──┘
doc               └──┘└─────┘           └──────┘        └──┘
430      (sum_card_order_of_eq_card_pow_eq_one hc0).symm
id        └──────────────────────────────────┘ └─┘ └──┘
src       └──────────────────────────────────┘     └──┘
typ       └──────────────────────────────────┘ └─┘ └──┘
431    ... = (((range c.succ).filter (∣ c)).erase d).sum
id              └───┘ └───┘ └────┘      └───┘   └─┘
src             └───┘  └───┘ └────┘       └───┘    └─┘
typ             └───┘ └───┘ └────┘      └───┘   └─┘
doc             └───┘        └────┘        └───┘
432        (λ m, (univ.filter (λ a : α, order_of a = m)).card) :
id               └──┘└─────┘          └──────┘     └──┘
src               └──┘└─────┘           └──────┘       └──┘
typ              └──┘└─────┘          └──────┘     └──┘
doc               └──┘└─────┘           └──────┘        └──┘
433      eq.symm (sum_subset (erase_subset _ _) (λ m hm₁ hm₂,
id       └─────┘  └────────┘  └──────────┘          └─┘ └─┘
src      └─────┘  └────────┘  └──────────┘
typ      └─────┘  └────────┘  └──────────┘          └─┘ └─┘
434        have m = d, by simp at *; cc,
id                
src                      └───────┘  └┘
typ                    └───────┘  └┘
doc                       └───────┘  └┘
txt                       └───────┘  └┘
par                       └───────┘  └┘
pid                           └──┘
st                       └────────────┘
435        by simp [*, finset.ext] at *; exact h0))
id                     └────────┘
src           └───────┘└────────┘└────┘  └────┘
typ           └───────┘└────────┘└────┘  └────┘
doc           └───────┘          └────┘  └────┘
txt           └───────┘          └────┘  └────┘
par           └───────┘          └────┘  └────┘
pid               └──┘          └──┘       
st           └──────────────────────────────────┘
436    ... ≤ (((range c.succ).filter (∣ c)).erase d).sum φ :
id              └───┘ └───┘ └────┘      └───┘   └─┘  
src             └───┘  └───┘ └────┘       └───┘    └─┘  
typ             └───┘ └───┘ └────┘      └───┘   └─┘  
doc             └───┘        └────┘        └───┘
437      sum_le_sum (λ m hm,
id       └────────┘     └┘
src      └────────┘
typ      └────────┘     └┘
438        have hmc : m ∣ c, by simp at hm; tauto,
id                      
src                            └────────┘  └───┘
typ                          └────────┘  └───┘
doc                             └────────┘  └───┘
txt                             └────────┘  └───┘
par                             └────────┘  └───┘
pid                                 └───┘
st                             └────────────────┘
439        (imp_iff_not_or.1 (card_order_of_eq_totient_aux₁ hn hmc)).elim
id          └────────────┘   └───────────────────────────┘ └┘ └─┘  └──┘
src         └────────────┘   └───────────────────────────┘         └──┘
typ         └────────────┘   └───────────────────────────┘ └┘ └─┘  └──┘
440          (λ h, by simp [nat.le_zero_iff.1 (le_of_not_gt h), nat.zero_le])
id                         └─────────────┘    └──────────┘    └─────────┘
src                   └────┘└─────────────┘└─┘ └──────────┘ └─┘└─────────┘
typ                  └────┘└─────────────┘└─┘ └──────────┘└─┘└─────────┘
doc                   └────┘               └─┘              └─┘           
txt                   └────┘               └─┘              └─┘           
par                   └────┘               └─┘              └─┘           
pid                                      └─┘              └─┘           
st                   └─────────────────────────────────────────────────────┘
441          (by simp [le_refl] {contextual := tt}))
id                     └─────┘                 └┘
src              └────┘└─────┘└┘ └────────────┘└┘
typ              └────┘└─────┘└┘ └────────────┘└┘
doc              └────┘       └┘ └────────────┘  
txt              └────┘       └┘ └────────────┘  
par              └────┘       └┘ └────────────┘  
pid                          └────────────┘  
st              └────────────────────────────────┘
442    ... < φ d + (((range c.succ).filter (∣ c)).erase d).sum φ :
id                 └───┘ └───┘ └────┘      └───┘   └─┘  
src                 └───┘  └───┘ └────┘       └───┘    └─┘  
typ                └───┘ └───┘ └────┘      └───┘   └─┘  
doc                   └───┘        └────┘        └───┘
443      lt_add_of_pos_left _ (totient_pos (nat.pos_of_ne_zero
id       └────────────────┘    └─────────┘  └────────────────┘
src      └────────────────┘    └─────────┘  └────────────────┘
typ      └────────────────┘    └─────────┘  └────────────────┘
444        (λ h, nat.pos_iff_ne_zero.1 hc0 (eq_zero_of_zero_dvd $ h ▸ hd))))
id              └─────────────────┘  └─┘  └─────────────────┘     └┘
src              └─────────────────┘       └─────────────────┘     
typ             └─────────────────┘  └─┘  └─────────────────┘     └┘
445    ... = (insert d (((range c.succ).filter (∣ c)).erase d)).sum φ : eq.symm (sum_insert (by simp))
id            └────┘     └───┘ └───┘ └────┘      └───┘    └─┘     └─────┘  └────────┘
src           └────┘      └───┘  └───┘ └────┘       └───┘     └─┘     └─────┘  └────────┘     └──┘
typ           └────┘     └───┘ └───┘ └────┘      └───┘    └─┘     └─────┘  └────────┘     └──┘
doc                       └───┘        └────┘        └───┘                                      └──┘
txt                                                                                             └──┘
par                                                                                             └──┘
st                                                                                             └───┘
446    ... = ((range c.succ).filter (∣ c)).sum φ : finset.sum_congr
id             └───┘ └───┘ └────┘      └─┘     └──────────────┘
src            └───┘  └───┘ └────┘       └─┘     └──────────────┘
typ            └───┘ └───┘ └────┘      └─┘     └──────────────┘
doc            └───┘        └────┘
447        (finset.insert_erase (mem_filter.2 ⟨mem_range.2 (lt_succ_of_le (le_of_dvd hc0 hd)), hd⟩)) (λ _ _, rfl)
id          └─────────────────┘  └────────┘   └───────┘   └───────────┘  └───────┘ └─┘ └┘    └┘          └─┘
src         └─────────────────┘  └────────┘   └───────┘   └───────────┘  └───────┘                         └─┘
typ         └─────────────────┘  └────────┘   └───────┘   └───────────┘  └───────┘ └─┘ └┘    └┘          └─┘
448    ... = c : sum_totient _
id              └─────────┘
src              └─────────┘
typ             └─────────┘
449  
450  lemma is_cyclic_of_card_pow_eq_one_le : is_cyclic α :=
id                                           └───────┘ 
src                                          └───────┘
typ                                          └───────┘ 
451  have (univ.filter (λ a : α, order_of a = fintype.card α)).nonempty,
id         └──┘└─────┘          └──────┘   └──────────┘   └──────┘
src        └──┘└─────┘           └──────┘    └──────────┘    └──────┘
typ        └──┘└─────┘          └──────┘   └──────────┘   └──────┘
doc        └──┘└─────┘           └──────┘     └──────────┘    └──────┘
452  from (card_pos.1 $
id         └──────┘
src        └──────┘
typ        └──────┘
453    by rw [card_order_of_eq_totient_aux₂ hn (dvd_refl _)];
id            └───────────────────────────┘ └┘  └──────┘
src       └──┘└───────────────────────────┘   └──────┘└──┘
typ       └──┘└───────────────────────────┘└┘ └──────┘└──┘
doc       └──┘                                        └──┘
txt       └──┘                                        └──┘
par       └──┘                                        └──┘
pid         └┘                                        └──┘
st       └────────────────────────────────────────────────┘└─
454    exact totient_pos (fintype.card_pos_iff.2 ⟨1⟩)),
id           └─────────┘  └──────────────────┘
src    └────┘└─────────┘ └──────────────────┘└─┘ └─┘
typ    └────┘└─────────┘ └──────────────────┘└─┘ └─┘
doc    └────┘                                └─┘ └─┘
txt    └────┘                                └─┘ └─┘
par    └────┘                                └─┘ └─┘
pid                                         └─┘ └─┘
st   ───────────────────────────────────────────────┘
455  let ⟨x, hx⟩ := this in
id   └─┘    └┘     └──┘
typ  └─┘    └┘     └──┘
456  is_cyclic_of_order_of_eq_card x (finset.mem_filter.1 hx).2
id   └───────────────────────────┘    └───────────────┘     
src  └───────────────────────────┘    └───────────────┘     
typ  └───────────────────────────┘    └───────────────┘     
457  
458  end totient
459  
460  lemma is_cyclic.card_order_of_eq_totient [group α] [is_cyclic α] [fintype α] [decidable_eq α]
id                                             └───┘    └───────┘    └─────┘    └──────────┘ 
src                                            └───┘     └───────┘     └─────┘     └──────────┘
typ                                            └───┘    └───────┘    └─────┘    └──────────┘ 
doc                                                                    └─────┘
461    {d : ℕ} (hd : d ∣ fintype.card α) : (univ.filter (λ a : α, order_of a = d)).card = totient d :=
id                    └──────────┘      └──┘└─────┘          └──────┘     └──┘   └─────┘ 
src                    └──────────┘       └──┘└─────┘           └──────┘       └──┘   └─────┘
typ                   └──────────┘      └──┘└─────┘          └──────┘     └──┘   └─────┘ 
doc                      └──────────┘       └──┘└─────┘           └──────┘        └──┘
462  card_order_of_eq_totient_aux₂ (λ n, is_cyclic.card_pow_eq_one_le) hd
id   └───────────────────────────┘      └──────────────────────────┘  └┘
src  └───────────────────────────┘       └──────────────────────────┘
typ  └───────────────────────────┘      └──────────────────────────┘  └┘
463  
464  end cyclic